awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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ˣ }
⊢ 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ˣ }
have 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ˣ }
Tactic: constructor
-- 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 :
  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ˣ }
have 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ˣ }
Tactic: rcases (QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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ˣ)
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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)
Tactic: have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := congr_arg Units.val hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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)
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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
Tactic: have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := congr_arg Units.inv hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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)
Tactic: rw [Units.val_pow_eq_pow_val] at hv
Cleared hypotheses: hv, hi
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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
Tactic: rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi
Cleared hypotheses: hi
-- 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ˣ }
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
⊢ 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 : ∀ (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ˣ }
Tactic: rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
        (hv.symm ▸ isIntegral_algebraMap) with
      ⟨v', rfl⟩
Cleared hypotheses: v, vi, iv, hx, hv, hi
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have vi₁ : v' * i' = 1
Tactic: rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi
Cleared hypotheses: iv, hx, hv, hi
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have iv₁ : i' * v' = 1
Tactic: rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at iv
Cleared hypotheses: hx, hv, hi
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have 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)
Tactic: rw [Units.val_mk, ← map_pow] at hv
Cleared hypotheses: hv, hi
-- 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
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 (γ := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
have h : Membership.mem (α := Rˣ) (γ := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
  (((powMonoidHom n : Rˣ →* Rˣ) : (a : Rˣ) → Rˣ) x : Rˣ)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1_1 D2_1 : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
h : Eq (α := (a : A) → M) ((fun (D : Derivation R A M) ↦ D.toFun) D1) ((fun (D : Derivation R A M) ↦ D.toFun) D2)
⊢ D1 = D2
have mk : ∀ (toLinearMap : A →ₗ[R] M) (map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M))
  (leibniz' :
    ∀ (a b : A),
      (toLinearMap : (a : A) → M) (a * b) =
        HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
          HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M))
  (h :
    Eq (α := (a : A) → M)
      ((fun (D : Derivation R A M) ↦ D.toFun)
        { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
      ((fun (D : Derivation R A M) ↦ D.toFun) D2)),
  { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } = D2
Tactic: cases D1
Cleared hypotheses: D1, h
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2_1 : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun) D2)
⊢ { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } = D2
have mk : ∀ (toLinearMap_1 : A →ₗ[R] M) (map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M))
  (leibniz'_1 :
    ∀ (a b : A),
      (toLinearMap_1 : (a : A) → M) (a * b) =
        HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
          HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M))
  (h :
    Eq (α := (a : A) → M)
      ((fun (D : Derivation R A M) ↦ D.toFun)
        { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
      ((fun (D : Derivation R A M) ↦ D.toFun)
        { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })),
  { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } =
    { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 }
Tactic: cases D2
Cleared hypotheses: D2, h
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap : A →ₗ[R] M
map_one_eq_zero' : Eq.{u_4 + 1} (α := M) ((toLinearMap : (a : A) → M) 1 : M) (0 : M)
leibniz' :
  ∀ (a b : A),
    (toLinearMap : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap : (a : A) → M) a : M)
toLinearMap_1 : A →ₗ[R] M
map_one_eq_zero'_1 : Eq.{u_4 + 1} (α := M) ((toLinearMap_1 : (a : A) → M) 1 : M) (0 : M)
leibniz'_1 :
  ∀ (a b : A),
    (toLinearMap_1 : (a : A) → M) (a * b) =
      HSMul.hSMul (β := M) a ((toLinearMap_1 : (a : A) → M) b : M) +
        HSMul.hSMul (β := M) b ((toLinearMap_1 : (a : A) → M) a : M)
h :
  Eq (α := (a : A) → M)
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' })
    ((fun (D : Derivation R A M) ↦ D.toFun)
      { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 })
⊢ { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' : Derivation R A M } =
    { toLinearMap := toLinearMap_1, map_one_eq_zero' := map_one_eq_zero'_1, leibniz' := leibniz'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]