awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ) (⇑(algebraMap R Sₚ) : (a : R) → Sₚ)
have rw : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)) : (a : R) → Sₚ)
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
⊢ IsPrincipalIdealRing Sₚ
have R₁ : ∀ (P : Ideal Sₚ),
  Membership.mem (γ := Finset (Ideal Sₚ))
      ({P ∈ {⊥} ∪ Multiset.toFinset (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) | P.IsPrime}) P ↔
    Membership.mem (γ := Set (Ideal Sₚ)) {I : Ideal Sₚ | I.IsPrime} P
Tactic: refine
    IsPrincipalIdealRing.of_finite_primes
      (Set.Finite.ofFinset
        {P ∈ {⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset | P.IsPrime}
        fun P => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
P : Ideal Sₚ
⊢ Membership.mem (γ := Finset (Ideal Sₚ))
      ({P ∈ {⊥} ∪ Multiset.toFinset (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) | P.IsPrime}) P ↔
    Membership.mem (γ := Set (Ideal Sₚ)) {I : Ideal Sₚ | I.IsPrime} P
have rw : (P = ⊥ ∨ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P) ∧
    P.IsPrime ↔
  P.IsPrime
Tactic: rw [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton, Set.mem_setOf,
    Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
⊢ IsPrincipalIdealRing R
have refine : ∀ (P : Ideal R) (hp : P.IsPrime) (hp₀ : P ≠ ⊥), Submodule.IsPrincipal P
Tactic: refine .of_prime_ne_bot fun P hp hp₀ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
⊢ Submodule.IsPrincipal P
have obtain : ∀ (x : R) (hx₁ : x ∈ P) (hx₂ : Prime x), Submodule.IsPrincipal P
Tactic: obtain ⟨x, hx₁, hx₂⟩ := hp.exists_mem_prime_of_ne_bot hp₀
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
⊢ Submodule.IsPrincipal P
have suffices : span {x} = P
Tactic: suffices Ideal.span {x} = P from this ▸ inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
⊢ span {x} = P
have this : IsPrime (α := R) (span {x})
Tactic: have := (Ideal.span_singleton_prime hx₂.ne_zero).mpr hx₂
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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
⊢ (↑(Subalgebra.toSubring (S.integer K)) : Set K) =
    (↑(⨅ (v : HeightOneSpectrum R),
          ⨅ (_ : v ∉ S), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
      Set K)
have h : ∀ (x : K),
  x ∈ (↑(Subalgebra.toSubring (S.integer K)) : Set K) ↔
    x ∈
      (↑(⨅ (v : HeightOneSpectrum R),
            ⨅ (_ : v ∉ S), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
        Set K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
⊢ Eq (α := Subalgebra R K) (Set.integer Set.univ K) ⊤
have h : ∀ (x : K), Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
x : K
⊢ Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊤ x
have h : Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x → Membership.mem (γ := Subalgebra R K) ⊤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
x : K
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
have h₁ : Membership.mem (γ := Subalgebra R K) ⊤ x → Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
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
⊢ Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊤ x
have 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 ℤ))
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
⊢ Eq (α := Subalgebra R K) (Set.integer ∅ K) ⊥
have h : ∀ (x : K), Membership.mem (γ := Subalgebra R K) (Set.integer ∅ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
x : K
⊢ Membership.mem (γ := Subalgebra R K) (Set.integer ∅ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊥ x
have 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 ℤ))}
            sorry),
      algebraMap_mem' := sorry }
    x ↔
  Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: simp only [Set.integer, Set.mem_empty_iff_false, not_false_eq_true, true_implies]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (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
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
have 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 ℤ))}
            sorry),
      algebraMap_mem' := sorry }
    x
Tactic: refine ⟨HeightOneSpectrum.mem_integers_of_valuation_le_one K x, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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
⊢ 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
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      ((↑(Units.mk0 (↑(↑x : ↥(S.integer K)) : K) sorry : Kˣ) : K) * (↑x.inv : K)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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 ℤ))
⊢ 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
have 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 ℤ))
Tactic: rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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 ℤ))
⊢ 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
have rw₂ : Eq (α := WithZero (Multiplicative ℤ))
  (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      1 :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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 ℤ))
⊢ 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
have rw₃ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
Tactic: rw [← map_mul, Units.val_mk0, Subtype.mk_eq_mk.mp x.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SInteger (goal)
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 := ⋯ } =
    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))ˣ }
have huv : (↑(↑{
            val :=
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                (↑(↑(x * x_1) : Kˣ) : K) sorry,
            inv :=
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                (↑(↑(x * x_1) : Kˣ)⁻¹ : K) sorry,
            val_inv := sorry, inv_val := sorry : (↥(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) sorry,
              inv :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x : Kˣ)⁻¹ : K)
                  sorry,
              val_inv := sorry, inv_val := sorry : (↥(S.integer K))ˣ }
            {
              val :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x) (↑(↑x_1 : Kˣ) : K)
                  sorry,
              inv :=
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra R K) (S.integer K) x)
                  (↑(↑x_1 : Kˣ)⁻¹ : K) sorry,
              val_inv := sorry, inv_val := sorry : (↥(S.integer K))ˣ }) :
        ↥(S.integer K)) :
    K)
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
v : HeightOneSpectrum R
x : Kˣ
⊢ (↑(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 ℤ))
have 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⁰) sorry :
                  ↥(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]