awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  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ˣ } →
    Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
      { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
h₁ :
  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.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
      { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ 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ˣ } ↔
    Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
      { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }

Tactic:
constructor
-- 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 :
  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ˣ }
h :
  ∀ (v i : K) (vi : v * i = 1) (iv : i * v = 1)
    (hx :
      Eq (α := Kˣ)
        (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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ˣ)),
    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 (QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩

Premises used: Subtype.mk.inj, Iff.mp, QuotientGroup.eq_one_iff
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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ˣ)
⊢ (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n) : K) =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)

Tactic:
have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := congr_arg Units.val hx
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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 :
  (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n) : K) =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)
⊢ (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n)⁻¹ : K) =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv

Tactic:
have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := congr_arg Units.inv hx
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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 :
  (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n) : K) =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)
hi :
  (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n)⁻¹ : K) =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
⊢ (↑{ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } : K) ^ n =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)

Tactic:
rw [Units.val_pow_eq_pow_val] at hv

Premises used: Units.val_pow_eq_pow_val
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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 :
  (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n) : K) =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)
hi :
  (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n)⁻¹ : K) =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
hv₁ :
  (↑{ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } : K) ^ n =
    (algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R)
⊢ (↑({ val := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n)⁻¹ : K) =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv

Tactic:
rw [Units.val_pow_eq_pow_val] at hv

Premises used: Units.val_pow_eq_pow_val
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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 :
  (↑{ val := v, inv := i, val_inv := vi, inv_val := iv : 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 := v, inv := i, val_inv := vi, inv_val := iv : Kˣ } ^ n)⁻¹ : K) =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
⊢ (↑{ val := i, inv := 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

Tactic:
rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi

Premises used: Units.inv_mk, inv_pow, Units.val_pow_eq_pow_val
-- 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ˣ }
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  Eq (α := Kˣ) (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) { val := 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 :
  (↑{ val := v, inv := i, val_inv := vi, inv_val := iv : 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 := 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 :
  ∀ (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ˣ }
⊢ 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 := v) hn.out
        (hv.symm ▸ isIntegral_algebraMap) with
      ⟨v', rfl⟩

Premises used: IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow, rfl, Fact.out
-- 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ˣ }
v' 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
⊢ v' * i' = 1

Tactic:
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi

Premises used: map_eq_one_iff, map_mul, FaithfulSMul.algebraMap_injective
-- 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ˣ }
v' 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
vi₁ : v' * i' = 1
⊢ HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1

Tactic:
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi

Premises used: map_eq_one_iff, map_mul, FaithfulSMul.algebraMap_injective
-- 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ˣ }
v' 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
vi₁ : v' * i' = 1
iv₁ : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1
⊢ 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ˣ)

Tactic:
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi

Premises used: map_eq_one_iff, map_mul, FaithfulSMul.algebraMap_injective
-- 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ˣ }
v' 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
vi₁ : v' * i' = 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ˣ)
⊢ 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)

Tactic:
rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi

Premises used: map_eq_one_iff, map_mul, FaithfulSMul.algebraMap_injective