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
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ˣ)
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)
⊢ 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

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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
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_1,
          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_1,
              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_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
⊢ i' * v' = 1

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

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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
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_1,
          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_1,
              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_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
iv₁ : i' * v' = 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_1,
          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 iv

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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
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_1,
          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_1,
              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_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
iv₁ : i' * v' = 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_1,
          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_1,
              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 iv

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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
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_1,
          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_1,
              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_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
iv₁ : i' * v' = 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_1,
          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_1,
              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)
⊢ 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_1 : Kˣ } :
          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 [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at iv

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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
vi : v' * i' = 1
iv_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1
iv : i' * v' = 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_1,
          inv_val := iv_1 } :
      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_1,
              inv_val := iv_1 : 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_1,
              inv_val := vi_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
⊢ Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) (v' ^ n) : K)
    ((algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R) : K)

Tactic:
rw [Units.val_mk, ← map_pow] at hv

Premises used: map_pow, Units.val_mk
-- 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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
vi : v' * i' = 1
iv_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1
iv : i' * v' = 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_1,
          inv_val := iv_1 } :
      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_1,
              inv_val := iv_1 : 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_1,
              inv_val := vi_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
hv₁ :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) (v' ^ n) : K)
    ((algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R) : K)
⊢ HPow.hPow (α := K)
      ((↑{ val := (algebraMap R K : (a : R) → K) i', inv := (algebraMap R K : (a : R) → K) v', val_inv := iv_1,
              inv_val := vi_1 : Kˣ } :
          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 [Units.val_mk, ← map_pow] at hv

Premises used: map_pow, Units.val_mk
-- 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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
vi : v' * i' = 1
iv_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1
iv : i' * v' = 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_1,
          inv_val := iv_1 } :
      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 :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) (v' ^ n) : K)
    ((algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R) : K)
hi :
  HPow.hPow (α := K)
      ((↑{ val := (algebraMap R K : (a : R) → K) i', inv := (algebraMap R K : (a : R) → K) v', val_inv := iv_1,
              inv_val := vi_1 : Kˣ } :
          K) :
        K)
      n =
    (algebraMap R K : (a : R) → K) { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }.inv
⊢ ((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }

Tactic:
simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv

Premises used: Units.ext_iff, FaithfulSMul.algebraMap_injective, Units.val_pow_eq_pow_val, powMonoidHom_apply
-- 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_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) v' : K) ((algebraMap R K : (a : R) → K) i' : K) = 1
vi : v' * i' = 1
iv_1 : HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) i' : K) ((algebraMap R K : (a : R) → K) v' : K) = 1
iv : i' * v' = 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_1,
          inv_val := iv_1 } :
      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 :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) (v' ^ n) : K)
    ((algebraMap R K : (a : R) → K) (↑{ val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ } : R) : K)
hi :
  HPow.hPow (α := K)
      ((↑{ val := (algebraMap R K : (a : R) → K) i', inv := (algebraMap R K : (a : R) → K) v', val_inv := iv_1,
              inv_val := vi_1 : 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:
exact ⟨⟨v', i', vi, iv⟩, by
      simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv⟩
-- 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
x : Rˣ
hx :
  ((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x =
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
h :
  Membership.mem (α := Rˣ) (γ := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    (((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x : 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ˣ }

Tactic:
rw [← 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
x : Rˣ
hx :
  ((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x =
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ Eq (α := Kˣ)
    (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ)
        (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
      Kˣ)
    (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ)
        (((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x) :
      Kˣ)

Tactic:
simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]

Premises used: RingHom.toMonoidHom_eq_coe, map_pow, powMonoidHom_apply
-- 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
x : Rˣ
hx :
  ((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x =
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
⊢ Membership.mem (α := Rˣ) (γ := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    (((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x : Rˣ)

Tactic:
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]⟩

Premises used: Iff.mpr, Subtype.mk_eq_mk