-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma isGermInjectiveAt_iff_of_isOpenImmersion {x : X} [IsOpenImmersion f] :
    Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
⊢ Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x) ↔ X.IsGermInjectiveAt x

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩

Result:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
⊢ X.IsGermInjectiveAt x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H :
  MorphismProperty.injective CommRingCat
    ((Scheme.Hom.appIso f ↑V).inv ≫
      Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Tactic:
simpa using H

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
⊢ X.IsGermInjectiveAt x

Tactic:
obtain ⟨U, hxU, hU, hU', H⟩ :=
  Y.exists_le_and_germ_injective (f.base x) (V := f.opensRange) ⟨x, rfl⟩

Result:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
U : Y.Opens
hxU : (ConcreteCategory.hom f.base) x ∈ U
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU))
⊢ X.IsGermInjectiveAt x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H :
  MorphismProperty.injective CommRingCat
    (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Tactic:
replace H := ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
  (f.appIso V).inv _).mpr H

Result:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H :
  MorphismProperty.injective CommRingCat
    ((Scheme.Hom.appIso f ↑V).inv ≫
      Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Proof state:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
V : ↑X.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ f ''ᵁ ↑V
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) x) hxU))
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x

Tactic:
obtain ⟨y, hy, e : f.base y = f.base x⟩ := hxU

Result:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) x
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) x) ⋯))
⊢ X.IsGermInjectiveAt x

Proof state:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
U : Y.Opens
hxU : (ConcreteCategory.hom f.base) x ∈ U
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU))
⊢ X.IsGermInjectiveAt x

Tactic:
obtain ⟨V, hV⟩ := (IsOpenImmersion.affineOpensEquiv f).surjective ⟨⟨U, hU⟩, hU'⟩

Result:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
U : Y.Opens
hxU : (ConcreteCategory.hom f.base) x ∈ U
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU))
V : ↑X.affineOpens
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨U, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯))
⊢ X.IsGermInjectiveAt y

Tactic:
refine ⟨V, hy, V.2, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯))
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Proof state:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
U : Y.Opens
hxU : (ConcreteCategory.hom f.base) x ∈ U
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU))
V : ↑X.affineOpens
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨U, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x

Tactic:
obtain rfl : f ''ᵁ V = U := Subtype.eq_iff.mp (Subtype.eq_iff.mp hV)

Result:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
V : ↑X.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ f ''ᵁ ↑V
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) x) hxU))
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
⊢ X.IsGermInjectiveAt x