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
v_1 : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a b : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        Eq (α := Multiplicative (ZMod n))
          (((v.valuationOfNeZeroMod n :
                  HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                    Multiplicative (ZMod n)) :
                (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    a
hy :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        Eq (α := Multiplicative (ZMod n))
          (((v.valuationOfNeZeroMod n :
                  HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                    Multiplicative (ZMod n)) :
                (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    b
v : HeightOneSpectrum R
hv : v ∉ S
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (a * b) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have rw : HMul.hMul (α := Multiplicative (ZMod n)) (β := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        a :
      Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        b :
      Multiplicative (ZMod n)) =
  1
Tactic: rw [map_mul, hx v hv, hy v hv, one_mul]
-- 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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x : HeightOneSpectrum R
h : x ∉ S
⊢ Eq (α := Multiplicative (ZMod n))
    (((x.valuationOfNeZeroMod n :
          HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
            Multiplicative (ZMod n)) :
        (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
      1)
    1
have rw : Eq (α := Multiplicative (ZMod n)) 1 1
Tactic: rw [map_one]
-- 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
v_1 : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        Eq (α := Multiplicative (ZMod n))
          (((v.valuationOfNeZeroMod n :
                  HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                    Multiplicative (ZMod n)) :
                (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    x
v : HeightOneSpectrum R
hv : v ∉ S
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        x⁻¹ :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have rw : Eq (α := Multiplicative (ZMod n))
  ((((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        x)⁻¹ :
    Multiplicative (ZMod n))
  (1 : Multiplicative (ZMod n))
Tactic: rw [map_inv, hx v hv, inv_one]
-- 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
v_1 : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        Eq (α := Multiplicative (ZMod n))
          (((v.valuationOfNeZeroMod n :
                  HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                    Multiplicative (ZMod n)) :
                (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    x
v : HeightOneSpectrum R
hv : v ∉ S
rw :
  Eq (α := Multiplicative (ZMod n))
    ((((v.valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          x)⁻¹ :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        x⁻¹ :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have rw₁ : Eq (α := Multiplicative (ZMod n)) 1⁻¹ 1
Tactic: rw [map_inv, hx v hv, inv_one]
-- 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
v_1 : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        Eq (α := Multiplicative (ZMod n))
          (((v.valuationOfNeZeroMod n :
                  HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                    Multiplicative (ZMod n)) :
                (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    x
v : HeightOneSpectrum R
hv : v ∉ S
rw :
  Eq (α := Multiplicative (ZMod n))
    ((((v.valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          x)⁻¹ :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
rw₁ : Eq (α := Multiplicative (ZMod n)) 1⁻¹ 1
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        x⁻¹ :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have rw₂ : Eq (α := Multiplicative (ZMod n)) 1 1
Tactic: rw [map_inv, hx v hv, inv_one]
-- 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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥(selmerGroup (S := S))
⊢ (fun (v : (↑S : Type u)) ↦
      (((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (↑(x * y) : Kˣ ⧸ (powMonoidHom n).range)) =
    HMul.hMul (α := (↑S : Type u) → Multiplicative (ZMod n))
      (fun (v : (↑S : Type u)) ↦
        (((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          (↑x : Kˣ ⧸ (powMonoidHom n).range))
      fun (v : (↑S : Type u)) ↦
      (((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (↑y : Kˣ ⧸ (powMonoidHom n).range)
have simp : (fun (v : (↑S : Type u)) ↦
    HMul.hMul (α := Multiplicative (ZMod n)) (β := Multiplicative (ZMod n))
      ((((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          (↑x : Kˣ ⧸ (powMonoidHom n).range) :
        Multiplicative (ZMod n))
      ((((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
              HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
                Multiplicative (ZMod n)) :
            (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
          (↑y : Kˣ ⧸ (powMonoidHom n).range) :
        Multiplicative (ZMod n))) =
  HMul.hMul (α := (↑S : Type u) → Multiplicative (ZMod n))
    (fun (v : (↑S : Type u)) ↦
      (((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (↑x : Kˣ ⧸ (powMonoidHom n).range))
    fun (v : (↑S : Type u)) ↦
    (((↑v : HeightOneSpectrum R).valuationOfNeZeroMod n :
          HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
            Multiplicative (ZMod n)) :
        (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
      (↑y : Kˣ ⧸ (powMonoidHom n).range)
Tactic: simp only [Subgroup.coe_mul, map_mul]
-- 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
S : Set (HeightOneSpectrum R)
n : ℕ
⊢ Eq.{v + 1} (α := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
have h : ∀ (val : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)))
  (hx :
    Membership.mem (γ :=
      Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
      (selmerGroup (S := S)) val),
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx) ↔
    Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
      (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx)
Tactic: ext ⟨_, hx⟩
-- 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
S : Set (HeightOneSpectrum R)
n : ℕ
val : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ :=
    Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    (selmerGroup (S := S)) val
⊢ Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx) ↔
    Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
      (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx)
have h : Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx) →
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
    (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx)
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
S : Set (HeightOneSpectrum R)
n : ℕ
val : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ :=
    Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    (selmerGroup (S := S)) val
h :
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx) →
    Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
      (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx)
⊢ Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx) ↔
    Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
      (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
      (Subtype.mk (p :=
        fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
        Membership.mem (γ :=
          Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
          (selmerGroup (S := S)) x)
        val hx)
have h₁ : Membership.mem (γ := Subgroup ↥(selmerGroup (S := S)))
    (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx) →
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx)
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
S : Set (HeightOneSpectrum R)
n : ℕ
val : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ :=
    Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    (selmerGroup (S := S)) val
hx' :
  Membership.mem (γ := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subtype.mk (p :=
      fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
      Membership.mem (γ :=
        Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
        (selmerGroup (S := S)) x)
      val hx)
v : HeightOneSpectrum R
h : v ∉ ∅
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        ((Subgroup.subtype (selmerGroup (S := S)) : (a : ↥selmerGroup) → Kˣ ⧸ (powMonoidHom n).range)
          (Subtype.mk (p :=
            fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
            Membership.mem (γ :=
              Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
              (selmerGroup (S := S)) x)
            val hx)) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have pos : ∀ (hv : v ∈ S),
  Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        ((Subgroup.subtype (selmerGroup (S := S)) : (a : ↥selmerGroup) → Kˣ ⧸ (powMonoidHom n).range)
          (Subtype.mk (p :=
            fun (x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))) ↦
            Membership.mem (γ :=
              Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
              (selmerGroup (S := S)) x)
            val hx)) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
Tactic: by_cases hv : v ∈ S
-- 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)
⊢ Eq.{u + 1} (α := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    (MonoidHom.range (G := Rˣ) (powMonoidHom n))
have h : ∀ (val inv : R) (val_inv : val * inv = 1) (inv_val : inv * val = 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ˣ } ↔
    Membership.mem (γ := Subgroup Rˣ) (MonoidHom.range (G := Rˣ) (powMonoidHom n))
      { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val : Rˣ }
Tactic: ext ⟨_, _, _, _⟩
-- 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
⊢ 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.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