-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    0
⊢ IsUnit.{u_1} (M := (↑(X.presheaf.stalk x) : Type u_1)) 0
have h₁ : 0 =
  HMul.hMul (α := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1)) (β :=
    (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
Tactic: convert! hx₁.mul hx₂