awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : ¬a = 0
H₁ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hb₁ : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x

Tactic:
rw [← h_frac] at H
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : ¬a = 0
H₁ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hb₁ : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac₁ : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
⊢ ¬a = 0

Tactic:
rw [← h_frac] at H
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
a b : A
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : ¬a = 0
neg :
  ∀ (n : ℕ) (u : Aˣ)
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
              ((algebraMap A K : (a : A) → K) b : K)) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)))
    (h_frac :
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) b : K) =
        x)
    (ha : ¬(↑u : A) * π ^ n = 0), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible ha hπ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
n : ℕ
u : Aˣ
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) b : K) =
    x
ha : ¬(↑u : A) * π ^ n = 0
neg :
  ∀ (m : ℕ) (w : Aˣ) (hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ((↑w : A) * π ^ m))
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
              ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K)) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)))
    (h_frac :
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
        x),
    ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
obtain ⟨m, w, rfl⟩ := eq_unit_mul_pow_irreducible (nonZeroDivisors.ne_zero hb) hπ

Premises used: nonZeroDivisors.ne_zero, IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) ((↑w : A) * π ^ m)
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)

Tactic:
replace hb := (mul_mem_nonZeroDivisors.mp hb).2
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x

Tactic:
rw [mul_comm (w : A) _, map_mul _ (u : A) _, map_mul _ _ (w : A), div_eq_mul_inv, mul_assoc,
      Valuation.map_mul, Integers.one_of_isUnit' u.isUnit (valuation_le_one _), one_mul,
      mul_inv, ← mul_assoc, Valuation.map_mul, map_mul, map_inv₀, map_inv₀,
      Integers.one_of_isUnit' w.isUnit (valuation_le_one _), inv_one, mul_one, ← div_eq_mul_inv,
      ← map_div₀, ← IsFractionRing.mk'_mk_eq_div hb,
      valuation_of_mk', map_pow, map_pow] at H

Premises used: Units.val, Valuation.Integers.one_of_isUnit', inv_one, mul_inv, mul_assoc, map_inv₀, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', map_pow, Valuation.map_mul, div_eq_mul_inv, IsFractionRing.mk'_mk_eq_div, map_mul, map_div₀, mul_comm, Units.isUnit, mul_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
h_frac₁ :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)

Tactic:
rw [mul_comm (w : A) _, map_mul _ (u : A) _, map_mul _ _ (w : A), div_eq_mul_inv, mul_assoc,
      Valuation.map_mul, Integers.one_of_isUnit' u.isUnit (valuation_le_one _), one_mul,
      mul_inv, ← mul_assoc, Valuation.map_mul, map_mul, map_inv₀, map_inv₀,
      Integers.one_of_isUnit' w.isUnit (valuation_le_one _), inv_one, mul_one, ← div_eq_mul_inv,
      ← map_div₀, ← IsFractionRing.mk'_mk_eq_div hb,
      valuation_of_mk', map_pow, map_pow] at H

Premises used: Units.val, Valuation.Integers.one_of_isUnit', inv_one, mul_inv, mul_assoc, map_inv₀, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', map_pow, Valuation.map_mul, div_eq_mul_inv, IsFractionRing.mk'_mk_eq_div, map_mul, map_div₀, mul_comm, Units.isUnit, mul_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
          ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
h_frac₁ :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb₁ : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
⊢ HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1

Tactic:
rw [mul_comm (w : A) _, map_mul _ (u : A) _, map_mul _ _ (w : A), div_eq_mul_inv, mul_assoc,
      Valuation.map_mul, Integers.one_of_isUnit' u.isUnit (valuation_le_one _), one_mul,
      mul_inv, ← mul_assoc, Valuation.map_mul, map_mul, map_inv₀, map_inv₀,
      Integers.one_of_isUnit' w.isUnit (valuation_le_one _), inv_one, mul_one, ← div_eq_mul_inv,
      ← map_div₀, ← IsFractionRing.mk'_mk_eq_div hb,
      valuation_of_mk', map_pow, map_pow] at H

Premises used: Units.val, Valuation.Integers.one_of_isUnit', inv_one, mul_inv, mul_assoc, map_inv₀, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', map_pow, Valuation.map_mul, div_eq_mul_inv, IsFractionRing.mk'_mk_eq_div, map_mul, map_div₀, mul_comm, Units.isUnit, mul_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
have v_π_lt_one := (intValuation_lt_one_iff_dvd (maximalIdeal A) π).mpr
          (dvd_of_eq ((irreducible_iff_uniformizer _).mp hπ))
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
v_π_lt_one :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
have v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0 := intValuation_ne_zero _ _ hπ.ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
v_π_lt_one :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
v_π_ne_zero :
  Ne (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
zify : LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)
⊢ m ≤ n

Tactic:
zify
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
v_π_lt_one :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
v_π_ne_zero :
  Ne (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
    (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) 0) : WithZero (Multiplicative ℤ))

Tactic:
rw [← WithZero.coe_one, div_eq_mul_inv, ← zpow_natCast, ← zpow_natCast, ← ofAdd_zero,
        ← zpow_neg, ← zpow_add₀ v_π_ne_zero, ← sub_eq_add_neg] at H

Premises used: zpow_natCast, ofAdd_zero, sub_eq_add_neg, div_eq_mul_inv, zpow_add₀, zpow_neg, WithZero.coe_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
v_π_lt_one :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
v_π_ne_zero :
  Ne (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
H₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
    (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) 0) : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [← WithZero.coe_one, div_eq_mul_inv, ← zpow_natCast, ← zpow_natCast, ← ofAdd_zero,
        ← zpow_neg, ← zpow_add₀ v_π_ne_zero, ← sub_eq_add_neg] at H

Premises used: zpow_natCast, ofAdd_zero, sub_eq_add_neg, div_eq_mul_inv, zpow_add₀, zpow_neg, WithZero.coe_one