awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
t : (↑Γ(X, U) : Type u)
s : ↥(Submonoid.powers f)
ht :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x ⋯) :
          (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
rw :
  Eq (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) 0 s) 0
rw₁ rw₂ : Eq.{u + 1} (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) 0 0
⊢ Eq (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) t s) 0

Tactic:
rw [H _ ht, IsLocalization.mk'_zero]

Premises used: IsLocalization.mk'_zero
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
⊢ ∃ (U : X.Opens) (hx : x ∈ U),
    IsAffineOpen U ∧
      Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
          (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
Scheme.IsGermInjectiveAt.cond

Premises used: AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
obtain :
  ∀ (U : X.Opens) (hx : x ∈ U) (hU : IsAffineOpen U)
    (H :
      Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
          (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))),
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧
        U ≤ V ∧
          Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ ∃ (U : X.Opens) (hx : x ∈ U),
    IsAffineOpen U ∧
      U ≤ V ∧
        Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
            (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)

Premises used: AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
obtain :
  ∀ (f : (↑Γ(X, U) : Type u)) (hf : X.basicOpen f ≤ V)
    (hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X) ∈ X.basicOpen f),
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧
        U ≤ V ∧
          Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ ∃ (U : X.Opens) (hx : x ∈ U),
    IsAffineOpen U ∧
      U ≤ V ∧
        Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
            (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f ≤ V
hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X) ∈ X.basicOpen f
⊢ ∃ (U : X.Opens) (hx : x ∈ U),
    IsAffineOpen U ∧
      U ≤ V ∧
        Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
            (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.injective_germ_basicOpen, And.intro, AlgebraicGeometry.Scheme.basicOpen, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
U : X.Opens
hx : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
f : (↑Γ(X, U) : Type u)
hf : X.basicOpen f ≤ V
hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X) ∈ X.basicOpen f
⊢ ∃ (U : X.Opens) (hx : x ∈ U),
    IsAffineOpen U ∧
      U ≤ V ∧
        Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
            (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
exact ⟨X.basicOpen f, hxf, hU.basicOpen f, hf, injective_germ_basicOpen U hU x hx f hxf H⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
obtain :
  ∀ (U : X.Opens) (hxU : x ∈ U) (hU : IsAffineOpen U)
    (H :
      Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
          (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))),
    Y.IsGermInjectiveAt (f x)
⊢ Y.IsGermInjectiveAt (f x)

Tactic:
obtain ⟨U, hxU, hU, H⟩ := X.exists_germ_injective x

Premises used: AlgebraicGeometry.Scheme.exists_germ_injective
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Y.IsGermInjectiveAt (f x)

Tactic:
⟨⟨f ''ᵁ U, ⟨x, hxU, rfl⟩, hU.image_of_isOpenImmersion f, ?_⟩⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, AlgebraicGeometry.Scheme.IsGermInjectiveAt.mk, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, And.intro, Exists.intro, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
refine :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U))) (Y := Y.presheaf.stalk (f x))
          (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
⊢ Y.IsGermInjectiveAt (f x)

Tactic:
refine ⟨⟨f ''ᵁ U, ⟨x, hxU, rfl⟩, hU.image_of_isOpenImmersion f, ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U))) (Y := Y.presheaf.stalk (f x))
          (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))

Tactic:
((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
    (f.stalkMap x)).mp ?_

Premises used: CommRingCat, CategoryTheory.MorphismProperty.injective, Iff.mp, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
refine :
  MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U)))
    (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x)
⊢ Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U))) (Y := Y.presheaf.stalk (f x))
          (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))

Tactic:
refine ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
    (f.stalkMap x)).mp ?_

Premises used: CommRingCat, CategoryTheory.MorphismProperty.injective, Iff.mp, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U)))
    (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x)

Tactic:
((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso U).inv _).mp ?_

Premises used: CommRingCat, CategoryTheory.MorphismProperty.injective, AlgebraicGeometry.Scheme.Hom.appIso, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
refine :
  MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier)
    (CategoryStruct.comp (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Scheme.Hom.appIso f U))
      (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x))
⊢ MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ U)))
    (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x)

Tactic:
refine ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso U).inv _).mp ?_

Premises used: CommRingCat, CategoryTheory.MorphismProperty.injective, AlgebraicGeometry.Scheme.Hom.appIso, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
inst_1 : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier)
    (CategoryStruct.comp (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Scheme.Hom.appIso f U))
      (Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
⊢ Y.IsGermInjectiveAt (f x) ↔ X.IsGermInjectiveAt x

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

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
refine : ∀ (H : Y.IsGermInjectiveAt (f x)), X.IsGermInjectiveAt x
⊢ Y.IsGermInjectiveAt (f x) ↔ X.IsGermInjectiveAt x

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H : Y.IsGermInjectiveAt (f x)
obtain :
  ∀ (U : Y.Opens) (hxU : Membership.mem (α := ↥Y) U (f x : ↥Y)) (hU : IsAffineOpen U)
    (hU' : U ≤ Scheme.Hom.opensRange f)
    (H :
      Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(Y.presheaf.stalk (f x)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hxU)) :
          (a : (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))),
    X.IsGermInjectiveAt x
⊢ X.IsGermInjectiveAt x

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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, DFunLike.coe, rfl
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
U : Y.Opens
hxU : Membership.mem (α := ↥Y) U (f x : ↥Y)
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hxU)) :
      (a : (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
obtain :
  ∀ (V : (↑X.affineOpens : Type u))
    (hV :
      Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        ((IsOpenImmersion.affineOpensEquiv f :
              (a : (↑X.affineOpens : Type u)) →
                { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
            V :
          { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
            (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) hU' :
          { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })),
    X.IsGermInjectiveAt x
⊢ X.IsGermInjectiveAt x

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

Premises used: OrderIso.surjective, Subtype.mk, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
U : Y.Opens
hxU : Membership.mem (α := ↥Y) U (f x : ↥Y)
hU : IsAffineOpen U
hU' : U ≤ Scheme.Hom.opensRange f
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hxU)) :
      (a : (↑(Y.presheaf.obj (Opposite.op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
V : (↑X.affineOpens : Type u)
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
⊢ f ''ᵁ (↑V : X.Opens) = U

Tactic:
Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)

Premises used: Subtype.ext_iff, Iff.mp