-- 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
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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ˣ }
Tactic: rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
        (hi.symm ▸ isIntegral_algebraMap) with
      ⟨i', rfl⟩
Cleared hypotheses: i, vi, iv, hx, hv, hi