awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if
          Eq.{u + 1} (α := R)
            (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1
            0 then
        0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk
                      (Ideal.span
                        {(Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰)
                              (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1})))) :
              ℤ)))
      (if
            Eq (α := R)
              ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R)
                  (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                      (↑x : K)).2 :
                R)
              (0 : R) then
          0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors
                      (Associates.mk
                        (Ideal.span
                          (singleton (α := R)
                            ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R)
                                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰)
                                    (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).2 :
                              R)))))) :
                ℤ)))⁻¹
have simp_rw : (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
  HMul.hMul (α := WithZero (Multiplicative ℤ))
    (if Eq.{u + 1} (α := R) (IsLocalization.sec R⁰ (↑x : K)).1 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ (↑x : K)).1})))) :
            ℤ)))
    (if Eq (α := R) ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R) (IsLocalization.sec R⁰ (↑x : K)).2 : R) (0 : R) then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk
                      (Ideal.span
                        (singleton (α := R)
                          ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R) (IsLocalization.sec R⁰ (↑x : K)).2 : R)))))) :
              ℤ)))⁻¹
Tactic: simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]
-- 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 ℤ)) =
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K)
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: classical
  rw [show v.valuation K x = _ * _ by rfl]
  rw [Units.val_inv_eq_inv_val]
  change _ = ite _ _ _ * (ite _ _ _)⁻¹
  simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]
-- 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ˣ
rw rw₁ 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 ℤ)) =
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K)
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: classical
  rw [show v.valuation K x = _ * _ by rfl]
  rw [Units.val_inv_eq_inv_val]
  change _ = ite _ _ _ * (ite _ _ _)⁻¹
  simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]
-- 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
⊢ valuationOfNeZeroToFun.{u, v} (K := K) v 1 = 1
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑1 : K) :
    WithZero (Multiplicative ℤ))
  ((↑1 : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]
-- 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 x_1 : Kˣ
⊢ v.valuationOfNeZeroToFun (x * x_1) = v.valuationOfNeZeroToFun x * v.valuationOfNeZeroToFun x_1
have rw : (↑(v.valuationOfNeZeroToFun (x * x_1)) : WithZero (Multiplicative ℤ)) =
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) *
    (↑(v.valuationOfNeZeroToFun x_1) : WithZero (Multiplicative ℤ))
Tactic: rw [← WithZero.coe_inj, WithZero.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x x_1 : Kˣ
⊢ (↑(v.valuationOfNeZeroToFun (x * x_1)) : WithZero (Multiplicative ℤ)) =
    (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) *
      (↑(v.valuationOfNeZeroToFun x_1) : WithZero (Multiplicative ℤ))
have 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 ℤ))
Tactic: simp only [valuationOfNeZeroToFun_eq]
-- 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 : Rˣ
⊢ 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 ℤ)
have 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 ℤ))
Tactic: rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]
-- 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 : 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 ℤ)) ∧
    ¬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 ℤ))
have 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 ℤ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬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 ℤ))
have 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 ℤ))
Tactic: obtain ⟨x, _, hx, _⟩ := x
Cleared hypotheses: x
-- 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 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 ℤ))
have 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 ℤ))
Tactic: change ¬v.valuation K (algebraMap R K x) < 1
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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
⊢ ¬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 ℤ))
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (hypothesis)
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 ℤ))
⊢ ¬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 ℤ))
have 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
Tactic: rw [map_one, map_mul] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
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
⊢ ¬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 ℤ))
have 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 ℤ))
Tactic: rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap]
-- 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 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
⊢ 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 ℤ))
have right : LE.le (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) inv : WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: gcongr
-- 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
n : ℕ
x : Kˣ
⊢ 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 ℤ) :
      ℤ)
have 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 : ℤ) : ℤ)
Tactic: simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]
-- 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
n : ℕ
x : Rˣ
⊢ 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))
        (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
          Kˣ ⧸ (powMonoidHom n).range) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have erw : Eq (α := Multiplicative (ZMod n))
  (((MonoidHom.comp
            (MulEquiv.toMonoidHom
              ((AddEquiv.toMultiplicative :
                  (a : ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ) ≃+ ZMod n) →
                    Multiplicative (ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ)) ≃* Multiplicative (ZMod n))
                (Int.quotientZMultiplesNatEquivZMod n)))
            (QuotientGroup.map (MonoidHom.range (G := Kˣ) (powMonoidHom n))
              ((AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
                (AddSubgroup.zmultiples (↑n : ℤ)))
              v.valuationOfNeZero sorry) :
          HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
            Multiplicative (ZMod n)) :
        (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
      (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
        Kˣ ⧸ (powMonoidHom n).range) :
    Multiplicative (ZMod n))
  (1 : Multiplicative (ZMod n))
Tactic: erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
    QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),
    valuation_of_unit_eq, QuotientGroup.mk_one, map_one]