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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥(selmerGroup (S := S))
⊢ (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:
rfl
-- 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
S : Set (HeightOneSpectrum R)
n : ℕ
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)
⊢ Eq.{v + 1} (α := Subgroup ↥(selmerGroup (S := S))) (MonoidHom.ker (valuation (S := S)))
    (Subgroup.subgroupOf (selmerGroup (S := ∅)) (selmerGroup (S := S)))

Tactic:
ext ⟨_, 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
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)
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)
⊢ 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
-- 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
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))
⊢ 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))

Tactic:
_
-- 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
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 ∉ ∅
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:
congr_fun hx' ⟨v, hv⟩

Premises used: Quotient.liftOn', AddCon.liftOn, Subtype.mk, congr_fun
-- 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
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 ∉ ∅
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:
exact congr_fun hx' ⟨v, hv⟩

Premises used: Subtype.mk, congr_fun
-- 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
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 ∉ ∅
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:
hx v 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
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 ∉ ∅
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:
exact hx v 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
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)))
      (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:
fun hx' => funext fun v => hx' v <| Set.notMem_empty v

Premises used: Set.Mem, setOf, funext, Set.preimage, Set.singleton, Set.notMem_empty, Subtype.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
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)))
      (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:
exact fun hx' => funext fun v => hx' v <| Set.notMem_empty v

Premises used: funext
-- 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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n_1 n : ℕ
⊢ Eq.{v + 1} (α := ↥(selmerGroup (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 := ∅)) x)
      (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) 1) :
        Kˣ ⧸ (powMonoidHom n).range)
      ⋯)
    1

Tactic:
simp only [map_one, QuotientGroup.mk_one, Subgroup.mk_eq_one]

Premises used: QuotientGroup.mk_one, map_one, Subgroup.mk_eq_one
-- 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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n_1 n : ℕ
x x_1 : Rˣ
⊢ 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 := ∅)) x)
      (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) (x * x_1)) :
        Kˣ ⧸ (powMonoidHom n).range)
      ⋯ =
    HMul.hMul (α := ↥(selmerGroup (S := ∅))) (β := ↥(selmerGroup (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 := ∅)) x)
          (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
            Kˣ ⧸ (powMonoidHom n).range)
          ⋯ :
        ↥(selmerGroup (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 := ∅)) x)
          (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x_1) :
            Kˣ ⧸ (powMonoidHom n).range)
          ⋯ :
        ↥(selmerGroup (S := ∅)))

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, map_mul, QuotientGroup.mk_mul,
    MulMemClass.mk_mul_mk]

Premises used: RingHom.toMonoidHom_eq_coe, map_mul, MulMemClass.mk_mul_mk, QuotientGroup.mk_mul
-- 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)
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ˣ }
⊢ Eq.{u + 1} (α := Subgroup Rˣ) (MonoidHom.ker.{u, v} (M := ↥(selmerGroup (S := ∅))) fromUnit)
    (MonoidHom.range (G := Rˣ) (powMonoidHom n))

Tactic:
ext ⟨_, _, _, _⟩