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
x x_1 : Kˣ
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(x * x_1) : K) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K) :
        WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (↑x_1 : K) :
        WithZero (Multiplicative ℤ))

Tactic:
exact map_mul _ _ _

Premises used: map_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
v : HeightOneSpectrum R
x : Kˣ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑(((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K) :
      WithZero (Multiplicative ℤ))

Tactic:
valuationOfNeZeroToFun_eq v x

Premises used: IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq
-- 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
x : Rˣ
rw :
  LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
        WithZero (Multiplicative ℤ))
      ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ)) ∧
    ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
          WithZero (Multiplicative ℤ))
        ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ Eq (α := Multiplicative ℤ)
    (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ)
        (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
      Multiplicative ℤ)
    (1 : Multiplicative ℤ)

Tactic:
rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]

Premises used: WithZero.coe_inj, Units.coe_map, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, eq_iff_le_not_lt
-- 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
x : Rˣ
left :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
right :
  ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
        WithZero (Multiplicative ℤ))
      ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
        WithZero (Multiplicative ℤ))
      ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ)) ∧
    ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
          WithZero (Multiplicative ℤ))
        ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

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
v : HeightOneSpectrum R
x : Rˣ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
v.valuation_le_one x

Premises used: Units.val, IsDedekindDomain.HeightOneSpectrum.valuation_le_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
x : Rˣ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
exact v.valuation_le_one x

Premises used: Units.val, IsDedekindDomain.HeightOneSpectrum.valuation_le_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
x : Rˣ
right :
  ∀ (x inv : R) (hx : x * inv = 1) (inv_val : inv * x = 1),
    ¬LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            (((↑(algebraMap R K) : R →* K) : (a : R) → K)
              (↑{ val := x, inv := inv, val_inv := hx, inv_val := inv_val : Rˣ } : R)) :
          WithZero (Multiplicative ℤ))
        ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (((↑(algebraMap R K) : R →* K) : (a : R) → K) (↑x : R)) :
        WithZero (Multiplicative ℤ))
      ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨x, _, hx, _⟩ := x
-- 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
x inv : R
hx : x * inv = 1
inv_val : inv * x = 1
right :
  ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) x) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (((↑(algebraMap R K) : R →* K) : (a : R) → K)
            (↑{ val := x, inv := inv, val_inv := hx, inv_val := inv_val : Rˣ } : R)) :
        WithZero (Multiplicative ℤ))
      ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
change ¬v.valuation K (algebraMap R K x) < 1

Premises used: Algebra.algebraMap, IsDedekindDomain.HeightOneSpectrum.valuation, DFunLike.coe
-- 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
x inv : R
hx : x * inv = 1
inv_val : inv * x = 1
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x * inv) : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))

Tactic:
apply_fun v.intValuation at hx

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation
-- 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
x inv : R
inv_val : inv * x = 1
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (x * inv) : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) =
    1

Tactic:
rw [map_one, map_mul] at hx

Premises used: map_mul, map_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
x inv : R
inv_val : inv * x = 1
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) =
    1
right :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ ¬LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) x) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, not_lt, IsDedekindDomain.HeightOneSpectrum.valuation, mul_one, DFunLike.coe
-- 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
x inv : R
inv_val : inv * x = 1
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) =
    1
right :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
gcongr
-- 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
x inv : R
inv_val : inv * x = 1
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) =
    1
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
v.intValuation_le_one _

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_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
x inv : R
inv_val : inv * x = 1
hx :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ)) =
    1
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact v.intValuation_le_one _

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_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
n : ℕ
x : Kˣ
simp :
  HSMul.hSMul (α := ℤ) (β := ℤ)
      (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x : Multiplicative ℤ) (↑n : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ)
      ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
          (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x : Multiplicative ℤ) :
        ℤ)
      ((↑n : ℤ) : ℤ)
⊢ Eq (α := ℤ)
    ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℤ) x (↑n : ℤ))
        (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x) :
      ℤ)
    ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
        (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ)
            (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) x) :
          Multiplicative ℤ) :
      ℤ)

Tactic:
simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]

Premises used: Int.toAdd_pow, 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
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ HSMul.hSMul (α := ℤ) (β := ℤ)
      (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x : Multiplicative ℤ) (↑n : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ)
      ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ)
          (((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ) x : Multiplicative ℤ) :
        ℤ)
      ((↑n : ℤ) : ℤ)

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
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ Membership.mem (α := Kˣ) (γ := Subgroup Kˣ)
    (Subgroup.comap v.valuationOfNeZero
      ((AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ)) (AddSubgroup.zmultiples (↑n : ℤ))))
    (((powMonoidHom n : Kˣ →* Kˣ) : (a : Kˣ) → Kˣ) x : Kˣ)

Tactic:
exact
          ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; 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
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x : HeightOneSpectrum R
h : x ∉ S
rw rw₁ : Eq (α := Multiplicative (ZMod n)) 1 1
⊢ 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

Tactic:
rw [map_one]

Premises used: map_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_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
rw₂ 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))

Tactic:
rw [map_inv, hx v hv, inv_one]

Premises used: map_inv, inv_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
S S' : Set (HeightOneSpectrum R)
n : ℕ
hS : S ≤ S'
⊢ LE.le.{v} (α := Subgroup (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    (selmerGroup (S := S)) (selmerGroup (S := S'))

Tactic:
fun _ hx v => hx v ∘ mt (@hS v)

Premises used: Set.Mem, setOf, Function.comp, mt
-- 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))
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)
⊢ (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)

Tactic:
simp only [Subgroup.coe_mul, map_mul]

Premises used: Subgroup.coe_mul, map_mul