-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ :=
    Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    (selmerGroup (S := S)) val
hx' :
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx)
v : HeightOneSpectrum R
h : v ∉ ∅
pos :
  ∀ (hv : v ∈ S),
    Eq (α := Multiplicative (ZMod n))
      (((v.valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          ((Subgroup.subtype (selmerGroup (S := S)) : (a : ↥selmerGroup) → Kˣ ⧸ (powMonoidHom n).range)
            (Subtype.mk (p :=
              fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
              Membership.mem (γ :=
                Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
                (selmerGroup (S := S)) x)
              val hx)) :
        Multiplicative (ZMod n))
      (1 : Multiplicative (ZMod n))
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        ((Subgroup.subtype (selmerGroup (S := S)) : (a : ↥selmerGroup) → Kˣ ⧸ (powMonoidHom n).range)
          (Subtype.mk (p :=
            fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
            Membership.mem (γ :=
              Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
              (selmerGroup (S := S)) x)
            val hx)) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have neg : ∀ (hv : v ∉ S),
  Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        ((Subgroup.subtype (selmerGroup (S := S)) : (a : ↥selmerGroup) → Kˣ ⧸ (powMonoidHom n).range)
          (Subtype.mk (p :=
            fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
            Membership.mem (γ :=
              Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
              (selmerGroup (S := S)) x)
            val hx)) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
Tactic: by_cases hv : v ∈ S