awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
x : K
h : Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x → Membership.mem (γ := Subalgebra R K) ⊤ x
h₁ : Membership.mem (γ := Subalgebra R K) ⊤ x → Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x
h₂ h₃ h₄ : Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x → Membership.mem (γ := Subalgebra R K) ⊤ x
h₅ h₆ : Membership.mem (γ := Subalgebra R K) ⊤ x → Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x
h₇ :
  Membership.mem (γ := Subalgebra R K) ⊤ x →
    ∀ v ∉ Set.univ,
      LE.le (α := WithZero (Multiplicative ℤ))
        (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
h₈ h₉ h₁₀ : Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x → Membership.mem (γ := Subalgebra R K) ⊤ x
h₁₁ :
  Membership.mem (γ := Subalgebra R K) ⊤ x →
    ∀ v ∉ Set.univ,
      LE.le (α := WithZero (Multiplicative ℤ))
        (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
h₁₂ h₁₃ h₁₄ h₁₅ h₁₆ :
  Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x → Membership.mem (γ := Subalgebra R K) ⊤ x
⊢ Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊤ x

Tactic:
tauto
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
h : ∀ (x : K), Membership.mem (γ := Subalgebra R K) (Set.integer ∅ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ Eq (α := Subalgebra R K) (Set.integer ∅ K) ⊥

Tactic:
ext x
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
x : K
h :
  Membership.mem (γ := Subalgebra R K)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subring.copy
              (⨅ (v : HeightOneSpectrum R),
                ⨅ (_ : True), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v)))
              {x : K |
                ∀ (v : HeightOneSpectrum R),
                  LE.le (α := WithZero (Multiplicative ℤ))
                    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                          (a : K) → WithZero (Multiplicative ℤ))
                        x :
                      WithZero (Multiplicative ℤ))
                    (1 : WithZero (Multiplicative ℤ))}
              ⋯),
        algebraMap_mem' := ⋯ }
      x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ Membership.mem (γ := Subalgebra R K) (Set.integer ∅ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
simp only [Set.integer, Set.mem_empty_iff_false, not_false_eq_true, true_implies]

Premises used: true_implies, Set.mem_empty_iff_false, not_false_eq_true, Set.integer
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
x : K
⊢ Membership.mem (γ := Subalgebra R K)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subring.copy
              (⨅ (v : HeightOneSpectrum R),
                ⨅ (_ : True), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v)))
              {x : K |
                ∀ (v : HeightOneSpectrum R),
                  LE.le (α := WithZero (Multiplicative ℤ))
                    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                          (a : K) → WithZero (Multiplicative ℤ))
                        x :
                      WithZero (Multiplicative ℤ))
                    (1 : WithZero (Multiplicative ℤ))}
              ⋯),
        algebraMap_mem' := ⋯ }
      x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
⟨HeightOneSpectrum.mem_integers_of_valuation_le_one K x, ?_⟩

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one, Iff.intro
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
x : K
h :
  Membership.mem (γ := Subalgebra R K) ⊥ x →
    Membership.mem (γ := Subalgebra R K)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subring.copy
              (⨅ (v : HeightOneSpectrum R),
                ⨅ (_ : True), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v)))
              {x : K |
                ∀ (v : HeightOneSpectrum R),
                  LE.le (α := WithZero (Multiplicative ℤ))
                    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                          (a : K) → WithZero (Multiplicative ℤ))
                        x :
                      WithZero (Multiplicative ℤ))
                    (1 : WithZero (Multiplicative ℤ))}
              ⋯),
        algebraMap_mem' := ⋯ }
      x
⊢ Membership.mem (γ := Subalgebra R K)
      {
        toSubsemiring :=
          Subring.toSubsemiring
            (Subring.copy
              (⨅ (v : HeightOneSpectrum R),
                ⨅ (_ : True), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v)))
              {x : K |
                ∀ (v : HeightOneSpectrum R),
                  LE.le (α := WithZero (Multiplicative ℤ))
                    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                          (a : K) → WithZero (Multiplicative ℤ))
                        x :
                      WithZero (Multiplicative ℤ))
                    (1 : WithZero (Multiplicative ℤ))}
              ⋯),
        algebraMap_mem' := ⋯ }
      x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
refine ⟨HeightOneSpectrum.mem_integers_of_valuation_le_one K x, ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
y : R
v : HeightOneSpectrum R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((AlgHom.toRingHom (Algebra.ofId R K) : (a : R) → K) y) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
v.valuation_le_one y

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
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
y : R
v : HeightOneSpectrum R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((AlgHom.toRingHom (Algebra.ofId R K) : (a : R) → K) y) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact v.valuation_le_one y

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : Kˣ
⊢ Membership.mem (γ := Set Kˣ)
      {x : Kˣ |
        ∀ v ∉ S,
          Eq (α := WithZero (Multiplicative ℤ))
            (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                  (a : K) → WithZero (Multiplicative ℤ))
                (↑x : K) :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ))}
      x ↔
    x ∈
      (↑(⨅ (v : HeightOneSpectrum R),
            ⨅ (_ : v ∉ S), ValuationSubring.unitGroup (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
        Set Kˣ)

Tactic:
simp only [mem_setOf, SetLike.mem_coe, Subgroup.mem_iInf, Valuation.mem_unitGroup_iff]

Premises used: Subgroup.mem_iInf, Valuation.mem_unitGroup_iff, Set.mem_setOf, SetLike.mem_coe
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
⊢ Eq (α := Subgroup Kˣ) (S.unit K)
    (⨅ (v : HeightOneSpectrum R),
      ⨅ (_ : v ∉ S), ValuationSubring.unitGroup (Valuation.valuationSubring (HeightOneSpectrum.valuation K v)))

Tactic:
Subgroup.copy_eq _ _ _

Premises used: Set.unit, Subgroup.copy_eq
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : ↥(S.unit K)
v : HeightOneSpectrum R
hv : v ∉ S
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (↑(↑x : Kˣ) : K) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
x.property v hv

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : (↥(S.integer K))ˣ
v : HeightOneSpectrum R
hv : v ∉ S
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((↑(Units.mk0 (↑(↑x : ↥(S.integer K)) : K) ⋯ : Kˣ) : K) * (↑x.inv : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((↑(↑x : ↥(S.integer K)) : K) * (↑x.inv : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        1 :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
rw₃ rw₄ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          (↑(Units.mk0 (↑(↑x : ↥(S.integer K)) : K) ⋯ : Kˣ) : K) :
        WithZero (Multiplicative ℤ))
      (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          (↑x.inv : K) :
        WithZero (Multiplicative ℤ)) =
    1

Tactic:
rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]

Premises used: map_mul, map_one, Subtype.mk_eq_mk, Iff.mp, Units.val_mk0, Units.val_inv
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x x_1 : ↥(S.unit K)
huv :
  (↑(↑{
              val :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                  (↑(↑(x * x_1) : Kˣ) : K) ⋯,
              inv :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                  (↑(↑(x * x_1) : Kˣ)⁻¹ : K) ⋯,
              val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ } :
          ↥(S.integer K)) :
      K) =
    (↑(↑(HMul.hMul (α := (↥(S.integer K))ˣ)
              {
                val :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x : Kˣ) : K)
                    ⋯,
                inv :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x : Kˣ)⁻¹ : K) ⋯,
                val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }
              {
                val :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x_1 : Kˣ) : K) ⋯,
                inv :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x_1 : Kˣ)⁻¹ : K) ⋯,
                val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }) :
          ↥(S.integer K)) :
      K)
⊢ {
      val :=
        Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑(x * x_1) : Kˣ) : K) ⋯,
      inv :=
        Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑(x * x_1) : Kˣ)⁻¹ : K)
          ⋯,
      val_inv := ⋯, inv_val := ⋯ } =
    HMul.hMul (α := (↥(S.integer K))ˣ)
      { val := Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x : Kˣ) : K) ⋯,
        inv :=
          Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x : Kˣ)⁻¹ : K) ⋯,
        val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }
      {
        val :=
          Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x_1 : Kˣ) : K) ⋯,
        inv :=
          Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x_1 : Kˣ)⁻¹ : K) ⋯,
        val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }

Tactic:
ext
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x x_1 : ↥(S.unit K)
⊢ (↑(↑{
              val :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                  (↑(↑(x * x_1) : Kˣ) : K) ⋯,
              inv :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                  (↑(↑(x * x_1) : Kˣ)⁻¹ : K) ⋯,
              val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ } :
          ↥(S.integer K)) :
      K) =
    (↑(↑(HMul.hMul (α := (↥(S.integer K))ˣ)
              {
                val :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x : Kˣ) : K)
                    ⋯,
                inv :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x : Kˣ)⁻¹ : K) ⋯,
                val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }
              {
                val :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x_1 : Kˣ) : K) ⋯,
                inv :=
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                    (↑(↑x_1 : Kˣ)⁻¹ : K) ⋯,
                val_inv := ⋯, inv_val := ⋯ : (↥(S.integer K))ˣ }) :
          ↥(S.integer K)) :
      K)

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
x : Kˣ
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)) :
            (a : R) → WithZero (Multiplicative ℤ))
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1 :
        WithZero (Multiplicative ℤ))
      ((↑(((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)).restrict R⁰) ⋯ :
                    ↥(R⁰ : Submonoid R) →* (WithZero (Multiplicative ℤ))ˣ) :
                  (a : ↥R⁰) → (WithZero (Multiplicative ℤ))ˣ)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2)⁻¹ :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

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
x : Kˣ
rw :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)) :
            (a : R) → WithZero (Multiplicative ℤ))
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1 :
        WithZero (Multiplicative ℤ))
      ((↑(((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)).restrict R⁰) ⋯ :
                    ↥(R⁰ : Submonoid R) →* (WithZero (Multiplicative ℤ))ˣ) :
                  (a : ↥R⁰) → (WithZero (Multiplicative ℤ))ˣ)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2) :
            WithZero (Multiplicative ℤ))⁻¹ :
        WithZero (Multiplicative ℤ))
⊢ (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)) :
            (a : R) → WithZero (Multiplicative ℤ))
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1 :
        WithZero (Multiplicative ℤ))
      ((↑(((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)).restrict R⁰) ⋯ :
                    ↥(R⁰ : Submonoid R) →* (WithZero (Multiplicative ℤ))ˣ) :
                  (a : ↥R⁰) → (WithZero (Multiplicative ℤ))ˣ)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2)⁻¹ :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

Tactic:
rw [Units.val_inv_eq_inv_val]

Premises used: Units.val_inv_eq_inv_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
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑1 : K) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ valuationOfNeZeroToFun.{u, v} (K := K) v 1 = 1

Tactic:
rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]

Premises used: WithZero.coe_inj, 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
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑1 : K) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
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 : HeightOneSpectrum R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑1 : K) :
      WithZero (Multiplicative ℤ))
    ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
exact 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 : HeightOneSpectrum R
x x_1 : Kˣ
rw :
  (↑(v.valuationOfNeZeroToFun (x * x_1)) : WithZero (Multiplicative ℤ)) =
    (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) *
      (↑(v.valuationOfNeZeroToFun x_1) : WithZero (Multiplicative ℤ))
⊢ v.valuationOfNeZeroToFun (x * x_1) = v.valuationOfNeZeroToFun x * v.valuationOfNeZeroToFun x_1

Tactic:
rw [← WithZero.coe_inj, WithZero.coe_mul]

Premises used: WithZero.coe_inj, WithZero.coe_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 x_1 : Kˣ
simp :
  ((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 ℤ))
⊢ (↑(v.valuationOfNeZeroToFun (x * x_1)) : WithZero (Multiplicative ℤ)) =
    (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) *
      (↑(v.valuationOfNeZeroToFun x_1) : WithZero (Multiplicative ℤ))

Tactic:
simp only [valuationOfNeZeroToFun_eq]

Premises used: 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 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:
map_mul _ _ _

Premises used: map_mul