[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


[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
q : R ⧸ J
a b : R
h : Setoid.r a b
⊢ ↑v a = ↑v (b + -(-a + b))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ J ≤ supp (comap (Ideal.Quotient.mk J) v)
[PROOFSTEP]
rw [comap_supp, ← Ideal.map_le_iff_le_comap]
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ Ideal.map (Ideal.Quotient.mk J) J ≤ supp v
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ ∀ (r : R ⧸ J), ↑(onQuot (comap (Ideal.Quotient.mk J) v) (_ : J ≤ supp (comap (Ideal.Quotient.mk J) v))) r = ↑v r
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ↑(onQuot (comap (Ideal.Quotient.mk J) v) (_ : J ≤ supp (comap (Ideal.Quotient.mk J) v))) (Quot.mk Setoid.r x) =
    ↑v (Quot.mk Setoid.r x)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp (onQuot v hJ) = Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp (onQuot v hJ) ≤ Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
rintro ⟨x⟩ hx
[GOAL]
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x✝ : R ⧸ J
x : R
hx : Quot.mk Setoid.r x ∈ supp (onQuot v hJ)
⊢ Quot.mk Setoid.r x ∈ Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case a.mk.a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x✝ : R ⧸ J
x : R
hx : Quot.mk Setoid.r x ∈ supp (onQuot v hJ)
⊢ Quot.mk Setoid.r x ∈ ↑(Ideal.Quotient.mk J) '' ↑(supp v)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ Ideal.map (Ideal.Quotient.mk J) (supp v) ≤ supp (onQuot v hJ)
[PROOFSTEP]
rw [Ideal.map_le_iff_le_comap]
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp v ≤ Ideal.comap (Ideal.Quotient.mk J) (supp (onQuot v hJ))
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x : R
hx : x ∈ supp v
⊢ x ∈ Ideal.comap (Ideal.Quotient.mk J) (supp (onQuot v hJ))
[PROOFSTEP]
exact hx
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ supp (onQuot v (_ : supp v ≤ supp v)) = 0
[PROOFSTEP]
rw [supp_quot]
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Ideal.map (Ideal.Quotient.mk (supp v)) (supp v) = 0
[PROOFSTEP]
exact Ideal.map_quotient_self _


[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {v | v.asIdeal ∣ I}
[PROOFSTEP]
rw [← Set.finite_coe_iff, Set.coe_setOf]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Finite { x // x.asIdeal ∣ I }
[PROOFSTEP]
haveI h_fin := fintypeSubtypeDvd I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Finite { x // x.asIdeal ∣ I }
[PROOFSTEP]
refine' Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Injective fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }
[PROOFSTEP]
intro v w hvw
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw :
  (fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }) v =
    (fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }) w
⊢ v = w
[PROOFSTEP]
simp at hvw
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (↑v).asIdeal = (↑w).asIdeal
⊢ v = w
[PROOFSTEP]
exact Subtype.coe_injective ((HeightOneSpectrum.ext_iff (R := R) ↑v ↑w).mpr hvw)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0
[PROOFSTEP]
have h_supp :
  {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ) = 0} =
    {v : HeightOneSpectrum R | v.asIdeal ∣ I} :=
  by
  ext v
  simp_rw [Int.coe_nat_eq_zero]
  exact Associates.count_ne_zero_iff_dvd hI v.irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}
[PROOFSTEP]
simp_rw [Int.coe_nat_eq_zero]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬count (Associates.mk v.asIdeal) (factors (Associates.mk I)) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}
[PROOFSTEP]
exact Associates.count_ne_zero_iff_dvd hI v.irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0
[PROOFSTEP]
rw [Filter.eventually_cofinite, h_supp]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
⊢ Set.Finite {v | v.asIdeal ∣ I}
[PROOFSTEP]
exact Ideal.finite_factors hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ {v | maxPowDividing v I ≠ 1} ⊆
    {v | ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠ 0}
[PROOFSTEP]
intro v hv h_zero
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
⊢ False
[PROOFSTEP]
have hv' : v.maxPowDividing I = 1 := by
  rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero, pow_zero _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
⊢ maxPowDividing v I = 1
[PROOFSTEP]
rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero, pow_zero _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
hv' : maxPowDividing v I = 1
⊢ False
[PROOFSTEP]
exact hv hv'
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    (mulSupport fun v =>
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
[PROOFSTEP]
rw [mulSupport]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {x | ↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) ≠ 1}
[PROOFSTEP]
simp_rw [Ne.def, zpow_ofNat, ← FractionalIdeal.coeIdeal_pow, FractionalIdeal.coeIdeal_eq_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {x | ¬x.asIdeal ^ Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)) = 1}
[PROOFSTEP]
exact finite_mulSupport hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    (mulSupport fun v =>
      ↑v.asIdeal ^ (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
[PROOFSTEP]
rw [mulSupport]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ↑x.asIdeal ^ (-↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)))) ≠ 1}
[PROOFSTEP]
simp_rw [zpow_neg, Ne.def, inv_eq_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ¬↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) = 1}
[PROOFSTEP]
exact finite_mulSupport_coe hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
have hf := finite_mulSupport hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
rw [← mul_finprod_cond_ne v hf, pow_add, pow_one, finprod_cond_ne _ _ hf]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
⊢ ¬v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
      maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
[PROOFSTEP]
intro h_contr
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
⊢ False
[PROOFSTEP]
have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
⊢ False
[PROOFSTEP]
obtain ⟨w, hw, hvw'⟩ := Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
⊢ False
[PROOFSTEP]
have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
⊢ False
[PROOFSTEP]
have hvw := Prime.dvd_of_dvd_pow hv_prime hvw'
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal ∣ w.asIdeal
⊢ False
[PROOFSTEP]
rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False
[PROOFSTEP]
exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext w v (Eq.symm hvw))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
[PROOFSTEP]
rw [Associates.mk_ne_zero, finprod_def]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ (if h : Set.Finite (mulSupport fun v => maxPowDividing v I) then ∏ i in Finite.toFinset h, maxPowDividing i I
    else 1) ≠
    0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∏ v in Finite.toFinset h✝, maxPowDividing v I ≠ 0
[PROOFSTEP]
rw [Finset.prod_ne_zero_iff]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∀ (a : HeightOneSpectrum R), a ∈ Finite.toFinset h✝ → maxPowDividing a I ≠ 0
[PROOFSTEP]
intro v _
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
v : HeightOneSpectrum R
a✝ : v ∈ Finite.toFinset h✝
⊢ maxPowDividing v I ≠ 0
[PROOFSTEP]
apply pow_ne_zero _ v.ne_bot
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : ¬Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_ne_zero := Associates.finprod_ne_zero I
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_dvd := finprod_mem_dvd v (Ideal.finite_mulSupport hI)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : maxPowDividing v I ∣ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_not_dvd := Ideal.finprod_not_dvd v I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : maxPowDividing v I ∣ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
h_not_dvd :
  ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
simp only [IsDedekindDomain.HeightOneSpectrum.maxPowDividing] at h_dvd h_ne_zero h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ∣
    ∏ᶠ (v : HeightOneSpectrum R),
      v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
h_not_dvd :
  ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← Associates.mk_dvd_mk] at h_dvd h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ∣
    Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)) ∣
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
simp only [Associates.dvd_eq_le] at h_dvd h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≤
    Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)) ≤
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le h_ne_zero hv] at h_dvd h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  ¬Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1 ≤
      Associates.count (Associates.mk v.asIdeal)
        (Associates.factors
          (Associates.mk
            (∏ᶠ (v : HeightOneSpectrum R),
              v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [not_le] at h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))) <
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
apply Nat.eq_of_le_of_lt_succ h_dvd h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I = I
[PROOFSTEP]
rw [← associated_iff_eq, ← Associates.mk_eq_mk_iff_associated]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) = Associates.mk I
[PROOFSTEP]
apply Associates.eq_of_eq_counts
[GOAL]
case ha
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
[PROOFSTEP]
apply Associates.finprod_ne_zero I
[GOAL]
case hb
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk I ≠ 0
[PROOFSTEP]
apply Associates.mk_ne_zero.mpr hI
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∀ (p : Associates (Ideal R)),
    Irreducible p →
      Associates.count p (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
        Associates.count p (Associates.factors (Associates.mk I))
[PROOFSTEP]
intro v hv
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
obtain ⟨J, hJv⟩ := Associates.exists_rep v
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
J : Ideal R
hJv : Associates.mk J = v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← hJv, Associates.irreducible_mk] at hv
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← hJv]
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ Associates.count (Associates.mk J)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
[PROOFSTEP]
apply Ideal.finprod_count ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ↑I
[PROOFSTEP]
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I)
[PROOFSTEP]
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(maxPowDividing a I)
[PROOFSTEP]
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow, zpow_ofNat]