awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₃ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
⊢ v.intValuationDef 1 = 1
have rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
⊢ v.intValuationDef 1 = 1
have rw₈ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
Tactic: rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₂ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₃ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
⊢ v.intValuationDef 1 = 1
have rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
⊢ v.intValuationDef 1 = 1
have rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
⊢ v.intValuationDef 1 = 1
have rw₈ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
Tactic: classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
have pos : ∀ (hx : x = 0),
  (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
have neg : ∀ (hx : ¬x = 0),
  (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
have pos : (if 0 * y = 0 then 0
  else
    exp
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0 * y})))) :
          ℤ))) =
  HMul.hMul (α := WithZero (Multiplicative ℤ))
    (if Eq.{u_1 + 1} (α := R) 0 0 then 0
    else
      exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
    (if y = 0 then 0
    else
      exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
Tactic: rw [hx, zero_mul, if_pos rfl, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
pos :
  (if 0 * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0 * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if Eq.{u_1 + 1} (α := R) 0 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
have pos₁ : (if Eq.{u_1 + 1} (α := R) 0 0 then 0
  else
    exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ))) =
  HMul.hMul (α := WithZero (Multiplicative ℤ))
    (if Eq.{u_1 + 1} (α := R) 0 0 then 0
    else
      exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
    (if y = 0 then 0
    else
      exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
Tactic: rw [hx, zero_mul, if_pos rfl, zero_mul]