awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 })
⊢ Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)

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

Premises used: Subtype.ext_iff, Iff.mp, 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))
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 })
hxU₁ : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
⊢ IsAffineOpen (f ''ᵁ (↑V : X.Opens))

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

Premises used: Subtype.ext_iff, Iff.mp, 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))
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 })
hxU₁ : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
hU₁ : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
⊢ f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f

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

Premises used: Subtype.ext_iff, Iff.mp, 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))
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 })
hxU₁ : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
hU₁ : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU'₁ : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
⊢ Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : 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 (f ''ᵁ (↑V : X.Opens)) (f x) hxU₁)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))

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

Premises used: Subtype.ext_iff, Iff.mp, 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))
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 })
hxU₁ : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
hU₁ : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU'₁ : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
H₁ :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : 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 (f ''ᵁ (↑V : X.Opens)) (f x) hxU₁)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
⊢ 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) (f ''ᵁ (↑V : X.Opens)) hU₁) hU'₁ :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })

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

Premises used: Subtype.ext_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
V : (↑X.affineOpens : Type u)
hxU : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : 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 (f ''ᵁ (↑V : X.Opens)) (f x) hxU)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : 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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
obtain :
  ∀ (y : ↥X) (hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)) (e : Eq (α := ↥Y) (f y : ↥Y) (f x : ↥Y))
    (H :
      Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : 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 ''ᵁ (↑V : X.Opens)))) (Y :=
              Y.presheaf.stalk (f x)) (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f x) ⋯)) :
          (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) →
            (↑(Y.presheaf.stalk (f x)) : Type u))),
    X.IsGermInjectiveAt x
⊢ X.IsGermInjectiveAt x

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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
e : Eq (α := ↥Y) (f y : ↥Y) (f x : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : 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 ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f x))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f x) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
obtain :
  ∀ (H : Y.IsGermInjectiveAt (f y)) (e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y))
    (H :
      Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
        (↑(Y.presheaf.stalk (f y)) : 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 ''ᵁ (↑V : X.Opens)))) (Y :=
              Y.presheaf.stalk (f y)) (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
          (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) →
            (↑(Y.presheaf.stalk (f y)) : Type u))),
    X.IsGermInjectiveAt y
⊢ X.IsGermInjectiveAt x

Tactic:
obtain rfl := f.isOpenEmbedding.injective e

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, rfl
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f y)) : 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 ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f y))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f y)) : Type u))
⊢ X.IsGermInjectiveAt y

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

Premises used: AlgebraicGeometry.Scheme.IsGermInjectiveAt.mk, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f y)) : 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 ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f y))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f y)) : Type u))
refine :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) (β :=
    (↑(X.presheaf.stalk y) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ (↑V : X.Opens) y hy)) :
      (a : (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) → (↑(X.presheaf.stalk y) : Type u))
⊢ X.IsGermInjectiveAt y

Tactic:
refine ⟨V, hy, V.2, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f y)) : 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 ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f y))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f y)) : 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 ''ᵁ (↑V : X.Opens))))
    (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y)

Tactic:
replace H := ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
    (f.stalkMap y)).mpr H
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  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 ''ᵁ (↑V : X.Opens))))
    (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Γ(X, (↑V : X.Opens)))
    (CategoryStruct.comp (Y := Γ(Y, f ''ᵁ (↑V : X.Opens))) (Iso.inv (Scheme.Hom.appIso f (↑V : X.Opens)))
      (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y))

Tactic:
replace H := ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso V).inv _).mpr H
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
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) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Γ(X, (↑V : X.Opens)))
    (CategoryStruct.comp (Y := Γ(Y, f ''ᵁ (↑V : X.Opens))) (Iso.inv (Scheme.Hom.appIso f (↑V : X.Opens)))
      (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y))
⊢ Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) (β :=
    (↑(X.presheaf.stalk y) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ (↑V : X.Opens) y hy)) :
      (a : (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) → (↑(X.presheaf.stalk y) : Type u))

Tactic:
simpa using H
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : ∀ (i : 𝒰.I₀), IsGermInjective.{u} (𝒰.X i)
x : ↥X
rw :
  X.IsGermInjectiveAt
    ((𝒰.f (Cover.idx 𝒰 x)) (Exists.choose (p := fun (y : ↥(𝒰.X (Cover.idx 𝒰 x))) ↦ (𝒰.f (Cover.idx 𝒰 x)) y = x) ⋯))
⊢ X.IsGermInjectiveAt x

Tactic:
rw [← (𝒰.covers x).choose_spec]

Premises used: Exists.choose_spec, AlgebraicGeometry.Scheme.Cover.covers