[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) x ≤ 1} ↔
    x✝ ∈
      ↑(⨅ (v : HeightOneSpectrum R) (_ : ¬v ∈ S),
          (Valuation.valuationSubring (HeightOneSpectrum.valuation v)).toSubring)
[PROOFSTEP]
simp [SetLike.mem_coe, Subring.mem_iInf]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ↑(Subalgebra.toSubring (integer S K)) =
    ↑(⨅ (v : HeightOneSpectrum R) (_ : ¬v ∈ S), (Valuation.valuationSubring (HeightOneSpectrum.valuation v)).toSubring)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ↑(Subalgebra.toSubring (integer S K)) ↔
    x✝ ∈
      ↑(⨅ (v : HeightOneSpectrum R) (_ : ¬v ∈ S),
          (Valuation.valuationSubring (HeightOneSpectrum.valuation v)).toSubring)
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : Kˣ
⊢ x✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑x = 1} ↔
    x✝ ∈
      ↑(⨅ (v : HeightOneSpectrum R) (_ : ¬v ∈ S),
          ValuationSubring.unitGroup (Valuation.valuationSubring (HeightOneSpectrum.valuation v)))
[PROOFSTEP]
simp only [mem_setOf, SetLike.mem_coe, Subgroup.mem_iInf, Valuation.mem_unitGroup_iff]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : { x // x ∈ integer S K }ˣ
v : HeightOneSpectrum R
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) * ↑(HeightOneSpectrum.valuation v) ↑x.inv = 1
[PROOFSTEP]
rw [Units.val_mk0, ← map_mul, Subtype.mk_eq_mk.mp x.val_inv, v.valuation.map_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : { x // x ∈ unit S K }
⊢ (fun x =>
        { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
          property :=
            (_ :
              ∀ (v : HeightOneSpectrum R),
                ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
      ((fun x =>
          {
            val :=
              { val := ↑↑x,
                property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
            inv :=
              { val := ↑(↑x)⁻¹,
                property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
            val_inv :=
              (_ :
                { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                    { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                  1),
            inv_val :=
              (_ :
                { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                    { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                  1) })
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case a.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : { x // x ∈ unit S K }
⊢ ↑↑((fun x =>
            { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
          ((fun x =>
              {
                val :=
                  { val := ↑↑x,
                    property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                inv :=
                  { val := ↑(↑x)⁻¹,
                    property :=
                      (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                val_inv :=
                  (_ :
                    { val := ↑↑x,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                        { val := ↑(↑x)⁻¹,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                      1),
                inv_val :=
                  (_ :
                    { val := ↑(↑x)⁻¹,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                        { val := ↑↑x,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                      1) })
            x✝)) =
    ↑↑x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : { x // x ∈ integer S K }ˣ
⊢ (fun x =>
        {
          val :=
            { val := ↑↑x,
              property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
          inv :=
            { val := ↑(↑x)⁻¹,
              property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
          val_inv :=
            (_ :
              { val := ↑↑x,
                    property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                  { val := ↑(↑x)⁻¹,
                    property :=
                      (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                1),
          inv_val :=
            (_ :
              { val := ↑(↑x)⁻¹,
                    property :=
                      (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                  { val := ↑↑x,
                    property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                1) })
      ((fun x =>
          { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
            property :=
              (_ :
                ∀ (v : HeightOneSpectrum R),
                  ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case a.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : { x // x ∈ integer S K }ˣ
⊢ ↑↑((fun x =>
            {
              val :=
                { val := ↑↑x,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
              inv :=
                { val := ↑(↑x)⁻¹,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
              val_inv :=
                (_ :
                  { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                      { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                    1),
              inv_val :=
                (_ :
                  { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                      { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                    1) })
          ((fun x =>
              { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                property :=
                  (_ :
                    ∀ (v : HeightOneSpectrum R),
                      ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
            x✝)) =
    ↑↑x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝¹ x✝ : { x // x ∈ unit S K }
⊢ Equiv.toFun
      {
        toFun := fun x =>
          {
            val :=
              { val := ↑↑x,
                property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
            inv :=
              { val := ↑(↑x)⁻¹,
                property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
            val_inv :=
              (_ :
                { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                    { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                  1),
            inv_val :=
              (_ :
                { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                    { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                  1) },
        invFun := fun x =>
          { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
            property :=
              (_ :
                ∀ (v : HeightOneSpectrum R),
                  ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
        left_inv :=
          (_ :
            ∀ (x : { x // x ∈ unit S K }),
              (fun x =>
                    { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                      property :=
                        (_ :
                          ∀ (v : HeightOneSpectrum R),
                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                  ((fun x =>
                      {
                        val :=
                          { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                        inv :=
                          { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                        val_inv :=
                          (_ :
                            { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                              1),
                        inv_val :=
                          (_ :
                            { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                              1) })
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : { x // x ∈ integer S K }ˣ),
              (fun x =>
                    {
                      val :=
                        { val := ↑↑x,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                      inv :=
                        { val := ↑(↑x)⁻¹,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                      val_inv :=
                        (_ :
                          { val := ↑↑x,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                              { val := ↑(↑x)⁻¹,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R),
                                      ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                            1),
                      inv_val :=
                        (_ :
                          { val := ↑(↑x)⁻¹,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R),
                                      ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                              { val := ↑↑x,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                            1) })
                  ((fun x =>
                      { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                        property :=
                          (_ :
                            ∀ (v : HeightOneSpectrum R),
                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                    x) =
                x) }
      (x✝¹ * x✝) =
    Equiv.toFun
        {
          toFun := fun x =>
            {
              val :=
                { val := ↑↑x,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
              inv :=
                { val := ↑(↑x)⁻¹,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
              val_inv :=
                (_ :
                  { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                      { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                    1),
              inv_val :=
                (_ :
                  { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                      { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                    1) },
          invFun := fun x =>
            { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
          left_inv :=
            (_ :
              ∀ (x : { x // x ∈ unit S K }),
                (fun x =>
                      { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                        property :=
                          (_ :
                            ∀ (v : HeightOneSpectrum R),
                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                    ((fun x =>
                        {
                          val :=
                            { val := ↑↑x,
                              property :=
                                (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                          inv :=
                            { val := ↑(↑x)⁻¹,
                              property :=
                                (_ :
                                  ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                          val_inv :=
                            (_ :
                              { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                  { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                1),
                          inv_val :=
                            (_ :
                              { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                  { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                1) })
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : { x // x ∈ integer S K }ˣ),
                (fun x =>
                      {
                        val :=
                          { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                        inv :=
                          { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                        val_inv :=
                          (_ :
                            { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                              1),
                        inv_val :=
                          (_ :
                            { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                              1) })
                    ((fun x =>
                        { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                          property :=
                            (_ :
                              ∀ (v : HeightOneSpectrum R),
                                ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                      x) =
                  x) }
        x✝¹ *
      Equiv.toFun
        {
          toFun := fun x =>
            {
              val :=
                { val := ↑↑x,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
              inv :=
                { val := ↑(↑x)⁻¹,
                  property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
              val_inv :=
                (_ :
                  { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                      { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                    1),
              inv_val :=
                (_ :
                  { val := ↑(↑x)⁻¹,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                      { val := ↑↑x,
                        property :=
                          (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                    1) },
          invFun := fun x =>
            { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
          left_inv :=
            (_ :
              ∀ (x : { x // x ∈ unit S K }),
                (fun x =>
                      { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                        property :=
                          (_ :
                            ∀ (v : HeightOneSpectrum R),
                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                    ((fun x =>
                        {
                          val :=
                            { val := ↑↑x,
                              property :=
                                (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                          inv :=
                            { val := ↑(↑x)⁻¹,
                              property :=
                                (_ :
                                  ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                          val_inv :=
                            (_ :
                              { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                  { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                1),
                          inv_val :=
                            (_ :
                              { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                  { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                1) })
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : { x // x ∈ integer S K }ˣ),
                (fun x =>
                      {
                        val :=
                          { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                        inv :=
                          { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                        val_inv :=
                          (_ :
                            { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                              1),
                        inv_val :=
                          (_ :
                            { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                              1) })
                    ((fun x =>
                        { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                          property :=
                            (_ :
                              ∀ (v : HeightOneSpectrum R),
                                ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                      x) =
                  x) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case a.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝¹ x✝ : { x // x ∈ unit S K }
⊢ ↑↑(Equiv.toFun
          {
            toFun := fun x =>
              {
                val :=
                  { val := ↑↑x,
                    property := (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                inv :=
                  { val := ↑(↑x)⁻¹,
                    property :=
                      (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                val_inv :=
                  (_ :
                    { val := ↑↑x,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                        { val := ↑(↑x)⁻¹,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                      1),
                inv_val :=
                  (_ :
                    { val := ↑(↑x)⁻¹,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                        { val := ↑↑x,
                          property :=
                            (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                      1) },
            invFun := fun x =>
              { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                property :=
                  (_ :
                    ∀ (v : HeightOneSpectrum R),
                      ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ unit S K }),
                  (fun x =>
                        { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                          property :=
                            (_ :
                              ∀ (v : HeightOneSpectrum R),
                                ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                      ((fun x =>
                          {
                            val :=
                              { val := ↑↑x,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                            inv :=
                              { val := ↑(↑x)⁻¹,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                            val_inv :=
                              (_ :
                                { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                    { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                  1),
                            inv_val :=
                              (_ :
                                { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                    { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                  1) })
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ integer S K }ˣ),
                  (fun x =>
                        {
                          val :=
                            { val := ↑↑x,
                              property :=
                                (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                          inv :=
                            { val := ↑(↑x)⁻¹,
                              property :=
                                (_ :
                                  ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                          val_inv :=
                            (_ :
                              { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                  { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                1),
                          inv_val :=
                            (_ :
                              { val := ↑(↑x)⁻¹,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                  { val := ↑↑x,
                                    property :=
                                      (_ :
                                        ∀ (v : HeightOneSpectrum R),
                                          ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                1) })
                      ((fun x =>
                          { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                            property :=
                              (_ :
                                ∀ (v : HeightOneSpectrum R),
                                  ¬v ∈ S →
                                    ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                        x) =
                    x) }
          (x✝¹ * x✝)) =
    ↑↑(Equiv.toFun
            {
              toFun := fun x =>
                {
                  val :=
                    { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                  inv :=
                    { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                  val_inv :=
                    (_ :
                      { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                          { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                        1),
                  inv_val :=
                    (_ :
                      { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                          { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                        1) },
              invFun := fun x =>
                { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
              left_inv :=
                (_ :
                  ∀ (x : { x // x ∈ unit S K }),
                    (fun x =>
                          { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                            property :=
                              (_ :
                                ∀ (v : HeightOneSpectrum R),
                                  ¬v ∈ S →
                                    ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                        ((fun x =>
                            {
                              val :=
                                { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                              inv :=
                                { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                              val_inv :=
                                (_ :
                                  { val := ↑↑x,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                      { val := ↑(↑x)⁻¹,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                    1),
                              inv_val :=
                                (_ :
                                  { val := ↑(↑x)⁻¹,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                      { val := ↑↑x,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                    1) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : { x // x ∈ integer S K }ˣ),
                    (fun x =>
                          {
                            val :=
                              { val := ↑↑x,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                            inv :=
                              { val := ↑(↑x)⁻¹,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                            val_inv :=
                              (_ :
                                { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                    { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                  1),
                            inv_val :=
                              (_ :
                                { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                    { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                  1) })
                        ((fun x =>
                            { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                              property :=
                                (_ :
                                  ∀ (v : HeightOneSpectrum R),
                                    ¬v ∈ S →
                                      ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                          x) =
                      x) }
            x✝¹ *
          Equiv.toFun
            {
              toFun := fun x =>
                {
                  val :=
                    { val := ↑↑x,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                  inv :=
                    { val := ↑(↑x)⁻¹,
                      property :=
                        (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                  val_inv :=
                    (_ :
                      { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                          { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                        1),
                  inv_val :=
                    (_ :
                      { val := ↑(↑x)⁻¹,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                          { val := ↑↑x,
                            property :=
                              (_ : ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                        1) },
              invFun := fun x =>
                { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) },
              left_inv :=
                (_ :
                  ∀ (x : { x // x ∈ unit S K }),
                    (fun x =>
                          { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                            property :=
                              (_ :
                                ∀ (v : HeightOneSpectrum R),
                                  ¬v ∈ S →
                                    ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                        ((fun x =>
                            {
                              val :=
                                { val := ↑↑x,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                              inv :=
                                { val := ↑(↑x)⁻¹,
                                  property :=
                                    (_ :
                                      ∀ (v : HeightOneSpectrum R),
                                        ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                              val_inv :=
                                (_ :
                                  { val := ↑↑x,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                      { val := ↑(↑x)⁻¹,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                    1),
                              inv_val :=
                                (_ :
                                  { val := ↑(↑x)⁻¹,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                      { val := ↑↑x,
                                        property :=
                                          (_ :
                                            ∀ (v : HeightOneSpectrum R),
                                              ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                    1) })
                          x) =
                      x),
              right_inv :=
                (_ :
                  ∀ (x : { x // x ∈ integer S K }ˣ),
                    (fun x =>
                          {
                            val :=
                              { val := ↑↑x,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) },
                            inv :=
                              { val := ↑(↑x)⁻¹,
                                property :=
                                  (_ :
                                    ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) },
                            val_inv :=
                              (_ :
                                { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } *
                                    { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } =
                                  1),
                            inv_val :=
                              (_ :
                                { val := ↑(↑x)⁻¹,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x⁻¹ ≤ 1) } *
                                    { val := ↑↑x,
                                      property :=
                                        (_ :
                                          ∀ (v : HeightOneSpectrum R),
                                            ¬v ∈ S → ↑(HeightOneSpectrum.valuation v) ↑↑x ≤ 1) } =
                                  1) })
                        ((fun x =>
                            { val := Units.mk0 ↑↑x (_ : ↑↑x = 0 → False),
                              property :=
                                (_ :
                                  ∀ (v : HeightOneSpectrum R),
                                    ¬v ∈ S →
                                      ↑(HeightOneSpectrum.valuation v) ↑(Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)) = 1) })
                          x) =
                      x) }
            x✝)
[PROOFSTEP]
rfl
