[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) = ↑(valuation v) ↑x
[PROOFSTEP]
rw [show v.valuation (x : K) = _ * _ by rfl]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuation v) ↑x = ?m.156670 * ?m.156673
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑↑(intValuation v).toMonoidWithZeroHom
        (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) R⁰)
                (_ : ∀ (s : { x // x ∈ R⁰ }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
            (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd)⁻¹
[PROOFSTEP]
rw [Units.val_inv_eq_inv_val]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑↑(intValuation v).toMonoidWithZeroHom
        (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst *
      (↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) R⁰)
                (_ : ∀ (s : { x // x ∈ R⁰ }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
            (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd))⁻¹
[PROOFSTEP]
change _ = ite _ _ _ * (ite _ _ _)⁻¹
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    (if (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst = 0 then 0
      else
        ↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk
                      (Ideal.span
                        {(Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst}))))))) *
      (if
            ↑(SubmonoidClass.subtype R⁰)
                (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd =
              0 then
          0
        else
          ↑(↑Multiplicative.ofAdd
              (-↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors
                      (Associates.mk
                        (Ideal.span
                          {↑(SubmonoidClass.subtype R⁰)
                              (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd})))))))⁻¹
[PROOFSTEP]
rw [IsLocalization.toLocalizationMap_sec]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    (if (IsLocalization.sec R⁰ ↑x).fst = 0 then 0
      else
        ↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).fst}))))))) *
      (if ↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0 then 0
        else
          ↑(↑Multiplicative.ofAdd
              (-↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors
                      (Associates.mk (Ideal.span {↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd})))))))⁻¹
[PROOFSTEP]
rw [if_neg <| IsLocalization.sec_fst_ne_zero le_rfl x.ne_zero, if_neg ?_]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑(↑Multiplicative.ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).fst})))))) *
      (↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk (Ideal.span {↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd})))))))⁻¹
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ¬↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ¬↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0
[PROOFSTEP]
exact nonZeroDivisors.coe_ne_zero _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ valuationOfNeZeroToFun v 1 = 1
[PROOFSTEP]
rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ↑(valuation v) ↑1 = ↑1
[PROOFSTEP]
exact map_one _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } (x✝¹ * x✝) =
    OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝¹ *
      OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝
[PROOFSTEP]
rw [← WithZero.coe_inj, WithZero.coe_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } (x✝¹ * x✝)) =
    ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝¹) *
      ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝)
[PROOFSTEP]
simp only [valuationOfNeZeroToFun_eq]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(valuation v) ↑(x✝¹ * x✝) = ↑(valuation v) ↑x✝¹ * ↑(valuation v) ↑x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuationOfNeZero v) (↑(Units.map ↑(algebraMap R K)) x) = 1
[PROOFSTEP]
rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuation v) (↑↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬↑(valuation v) (↑↑(algebraMap R K) ↑x) < ↑1
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuation v) (↑↑(algebraMap R K) ↑x) ≤ ↑1
[PROOFSTEP]
exact v.valuation_le_one x
[GOAL]
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬↑(valuation v) (↑↑(algebraMap R K) ↑x) < ↑1
[PROOFSTEP]
cases' x with x _ hx _
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬↑(valuation v) (↑↑(algebraMap R K) ↑{ val := x, inv := inv✝, val_inv := hx, inv_val := inv_val✝ }) < ↑1
[PROOFSTEP]
change ¬v.valuation (algebraMap R K x) < 1
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
apply_fun v.intValuation at hx 
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) (x * inv✝) = ↑(intValuation v) 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
rw [map_one, map_mul] at hx 
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) x * ↑(intValuation v) inv✝ = 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
rw [not_lt, ← hx, ← mul_one <| v.valuation _, valuation_of_algebraMap,
  mul_le_mul_left₀ <| left_ne_zero_of_mul_eq_one hx]
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) x * ↑(intValuation v) inv✝ = 1
⊢ ↑(intValuation v) inv✝ ≤ 1
[PROOFSTEP]
exact v.int_valuation_le_one _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
⊢ MonoidHom.range (powMonoidHom n) ≤
    Subgroup.comap (valuationOfNeZero v) (↑AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ ↑(powMonoidHom n) x ∈ Subgroup.comap (valuationOfNeZero v) (↑AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))
[PROOFSTEP]
exact ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ (fun x => x • ↑n) (↑(valuationOfNeZero v) x) = ↑Multiplicative.toAdd (↑(valuationOfNeZero v) (↑(powMonoidHom n) x))
[PROOFSTEP]
simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ ↑(valuationOfNeZero v) x • ↑n = ↑Multiplicative.toAdd (↑(valuationOfNeZero v) x) * ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ ↑(valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1
[PROOFSTEP]
rw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
  QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)), valuation_of_unit_eq, QuotientGroup.mk_one,
  map_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : a✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1}
hy : b✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1}
v : HeightOneSpectrum R
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (a✝ * b✝) = 1
[PROOFSTEP]
rw [map_mul, hx v hv, hy v hv, one_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝¹ : HeightOneSpectrum R
x✝ : ¬x✝¹ ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod x✝¹ n) 1 = 1
[PROOFSTEP]
rw [map_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx :
  x✝ ∈
    {
          toSubsemigroup :=
            {
              carrier :=
                {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1},
              mul_mem' :=
                (_ :
                  ∀ {a b : Kˣ ⧸ MonoidHom.range (powMonoidHom n)},
                    a ∈
                        {x |
                          ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1} →
                      b ∈
                          {x |
                            ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1} →
                        ∀ (v : HeightOneSpectrum R),
                          ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (a * b) = 1) },
          one_mem' :=
            (_ :
              ∀ (x : HeightOneSpectrum R),
                ¬x ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod x n) 1 = 1) }.toSubsemigroup.carrier
v : HeightOneSpectrum R
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x✝⁻¹ = 1
[PROOFSTEP]
rw [map_inv, hx v hv, inv_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : { x // x ∈ selmerGroup }
⊢ OneHom.toFun
      { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
        map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
          map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
          map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
        y
[PROOFSTEP]
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, map_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : { x // x ∈ selmerGroup }
⊢ (fun v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x * ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑y) =
    (fun v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) * fun v =>
      ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
⊢ MonoidHom.ker valuation = Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
ext ⟨_, hx⟩
[GOAL]
case h.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ MonoidHom.ker valuation ↔
    { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ MonoidHom.ker valuation →
    { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
intro hx' v _
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
by_cases hv : v ∈ S
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
hv : v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
exact congr_fun hx' ⟨v, hv⟩
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
exact hx v hv
[GOAL]
case h.mk.mpr
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup →
    { val := val✝, property := hx } ∈ MonoidHom.ker valuation
[PROOFSTEP]
exact fun hx' => funext fun v => hx' v <| Set.not_mem_empty v
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n✝ n : ℕ
⊢ (fun x =>
        { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
          property :=
            (_ :
              ∀ (v : HeightOneSpectrum R),
                ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) })
      1 =
    1
[PROOFSTEP]
simp only [map_one, QuotientGroup.mk_one, Subgroup.mk_eq_one_iff]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n✝ n : ℕ
x✝¹ x✝ : Rˣ
⊢ OneHom.toFun
      {
        toFun := fun x =>
          { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
            property :=
              (_ :
                ∀ (v : HeightOneSpectrum R),
                  ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
        map_one' :=
          (_ :
            { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                property :=
                  (_ :
                    ∀ (v : HeightOneSpectrum R),
                      ¬v ∈ ∅ →
                        ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
              1) }
      (x✝¹ * x✝) =
    OneHom.toFun
        {
          toFun := fun x =>
            { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
          map_one' :=
            (_ :
              { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ ∅ →
                          ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
                1) }
        x✝¹ *
      OneHom.toFun
        {
          toFun := fun x =>
            { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
          map_one' :=
            (_ :
              { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ ∅ →
                          ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
                1) }
        x✝
[PROOFSTEP]
simp only [RingHom.toMonoidHom_eq_coe, map_mul, MonoidHom.mem_range, powMonoidHom_apply, QuotientGroup.mk_mul,
  Submonoid.mk_mul_mk]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
⊢ MonoidHom.ker fromUnit = MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
ext ⟨_, _, _, _⟩
[GOAL]
case h.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit ↔
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
intro hx
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases(QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := by exact congr_arg Units.val hx
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(?m.1066492 ^ n) = ↑(algebraMap R K) ?m.1066434
[PROOFSTEP]
exact congr_arg Units.val hx
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := by exact congr_arg Units.inv hx
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(?m.1219650 ^ n)⁻¹ = ↑(algebraMap R K) ?m.1219637
[PROOFSTEP]
exact congr_arg Units.inv hx
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [Units.val_pow_eq_pow_val] at hv 
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi 
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := i, inv := v, val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
    (hv.symm ▸ isIntegral_algebraMap) with
  ⟨v', rfl⟩
[GOAL]
case h.mk.mp.intro.mk.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
i : K
v' : R
vi : ↑(algebraMap R K) v' * i = 1
iv : i * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := i, inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
    (hi.symm ▸ isIntegral_algebraMap) with
  ⟨i', rfl⟩
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
iv : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← map_mul, map_eq_one_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K] at vi 
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← map_mul, map_eq_one_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K] at iv 
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [Units.val_mk, ← map_pow] at hv 
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv : ↑(algebraMap R K) (v' ^ n) = ↑(algebraMap R K) val✝
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
exact
  ⟨⟨v', i', vi, iv⟩, by
    simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
      NoZeroSMulDivisors.algebraMap_injective R K hv⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv : ↑(algebraMap R K) (v' ^ n) = ↑(algebraMap R K) val✝
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ ↑(powMonoidHom n) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
[PROOFSTEP]
simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
  NoZeroSMulDivisors.algebraMap_injective R K hv
[GOAL]
case h.mk.mpr
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n) →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case h.mk.mpr.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
rw [← hx]
[GOAL]
case h.mk.mpr.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(powMonoidHom n) x ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
exact
  Subtype.mk_eq_mk.mpr <|
    (QuotientGroup.eq_one_iff _).mpr
      ⟨Units.map (algebraMap R K) x, by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(powMonoidHom n) (↑(Units.map ↑(algebraMap R K)) x) = ↑(Units.map ↑(algebraMap R K)) (↑(powMonoidHom n) x)
[PROOFSTEP]
simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective ↑fromUnitLift
[PROOFSTEP]
dsimp only [fromUnitLift, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective
    (↑(QuotientGroup.kerLift fromUnit) ∘
      ↑(MulEquiv.symm
          (QuotientGroup.quotientMulEquivOfEq (_ : MonoidHom.ker fromUnit = MonoidHom.range (powMonoidHom n)))))
[PROOFSTEP]
exact Function.Injective.comp (QuotientGroup.kerLift_injective _) (MulEquiv.injective _)
