awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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))
⊢ 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
have 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
Tactic: rw [H _ ht, IsLocalization.mk'_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ 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
have rw₁ : Eq.{u + 1} (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) 0 0
Tactic: rw [H _ ht, IsLocalization.mk'_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
V : X.Opens
hxV : x ∈ V
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨U, hx, hU, H⟩ := Scheme.IsGermInjectiveAt.cond (x := x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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))
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨f, hf, hxf⟩ := hU.exists_basicOpen_le ⟨x, hxV⟩ hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ Y.IsGermInjectiveAt (f x)
have 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)
Tactic: obtain ⟨U, hxU, hU, H⟩ := X.exists_germ_injective x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
have 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) sorry)) :
    (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ U))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
Tactic: refine ⟨⟨f ''ᵁ U, ⟨x, hxU, rfl⟩, hU.image_of_isOpenImmersion f, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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))
have 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) sorry ≫ Scheme.Hom.stalkMap f x)
Tactic: refine ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
    (f.stalkMap x)).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
have 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) sorry ≫ Scheme.Hom.stalkMap f x))
Tactic: refine ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso U).inv _).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
⊢ Y.IsGermInjectiveAt (f x) ↔ X.IsGermInjectiveAt x
have refine : ∀ (H : Y.IsGermInjectiveAt (f x)), X.IsGermInjectiveAt x
Tactic: refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H : Y.IsGermInjectiveAt (f x)
⊢ X.IsGermInjectiveAt x
have 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
Tactic: obtain ⟨U, hxU, hU, hU', H⟩ :=
    Y.exists_le_and_germ_injective (f x) (V := f.opensRange) ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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))
⊢ X.IsGermInjectiveAt x
have 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
Tactic: obtain ⟨V, hV⟩ := (IsOpenImmersion.affineOpensEquiv f).surjective ⟨⟨U, hU⟩, hU'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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 })
⊢ X.IsGermInjectiveAt x
have hxU₁ : 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)
Cleared hypotheses: U, hxU, hU, hU', H, hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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)
⊢ X.IsGermInjectiveAt x
have hU₁ : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
Tactic: obtain rfl : f ''ᵁ V = U := Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)
Cleared hypotheses: U, hxU, hU, hU', H, hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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))
⊢ X.IsGermInjectiveAt x
have hU'₁ : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
Tactic: obtain rfl : f ''ᵁ V = U := Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)
Cleared hypotheses: U, hxU, hU, hU', H, hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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
⊢ X.IsGermInjectiveAt x
have 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))
Tactic: obtain rfl : f ''ᵁ V = U := Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)
Cleared hypotheses: U, hxU, hU, hU', H, hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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))
⊢ X.IsGermInjectiveAt x
have 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 })
Tactic: obtain rfl : f ''ᵁ V = U := Subtype.ext_iff.mp (Subtype.ext_iff.mp hV)
Cleared hypotheses: U, hxU, hU, hU', H, hV