-- Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup
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
n : ℕ
hn : Fact (0 < n)
val inv : R
val_inv : val * inv = 1
inv_val : inv * val = 1
hx_1 :
  Membership.mem (γ := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
i : K
v' : R
vi : HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) v' : K) i = 1
iv : HMul.hMul (β := K) i ((algebraMap R K : (a : R) → K) v' : K) = 1
hx :
  Eq.{v + 1} (α := Kˣ)
    (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ)
        { val := (algebraMap R K : (a : R) → K) v', inv := i, val_inv := vi, inv_val := iv } :
      Kˣ)
    (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ)
        { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } :
      Kˣ)
hv :
  HPow.hPow (α := K)
      ((↑{ val := (algebraMap R K : (a : R) → K) v', inv := i, val_inv := vi, inv_val := iv : Kˣ } : K) : K) n =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)
hi :
  (↑{ val := i, inv := (algebraMap R K : (a : R) → K) v', val_inv := iv, inv_val := vi : Kˣ } : K) ^ n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
h :
  ∀ (i' : R)
    (vi :
      HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1)
    (iv :
      HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1)
    (hx :
      Eq.{v + 1} (α := Kˣ)
        (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ)
            { val := (algebraMap R K : (a : R) → K) v', inv := (algebraMap R K : (a : R) → K) i', val_inv := vi,
              inv_val := iv } :
          Kˣ)
        (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ)
            { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } :
          Kˣ))
    (hv :
      HPow.hPow (α := K)
          ((↑{ val := (algebraMap R K : (a : R) → K) v', inv := (algebraMap R K : (a : R) → K) i', val_inv := vi,
                  inv_val := iv : Kˣ } :
              K) :
            K)
          n =
        (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R))
    (hi :
      HPow.hPow (α := K)
          ((↑{ val := (algebraMap R K : (a : R) → K) i', inv := (algebraMap R K : (a : R) → K) v', val_inv := iv,
                  inv_val := vi : Kˣ } :
              K) :
            K)
          n =
        (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv),
    Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
      { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }

Tactic:
rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
        (hi.symm ▸ isIntegral_algebraMap) with
      ⟨i', rfl⟩

Premises used: IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow, rfl, Fact.out