awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have 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 ℤ))
Tactic: rw [← h_frac] at H
Cleared hypotheses: H, hb, h_frac, ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have 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
Tactic: obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible ha hπ
Cleared hypotheses: a, H, h_frac, ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have 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
Tactic: obtain ⟨m, w, rfl⟩ := eq_unit_mul_pow_irreducible (nonZeroDivisors.ne_zero hb) hπ
Cleared hypotheses: b, hb, H, h_frac
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have hb₁ : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
Tactic: replace hb := (mul_mem_nonZeroDivisors.mp hb).2
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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)
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have 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
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
Cleared hypotheses: H, h_frac, hb
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ m ≤ n
have v_π_lt_one : 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π))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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 ℤ))
⊢ m ≤ n
have v_π_ne_zero : 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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ℤ))
⊢ m ≤ n
have zify : LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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 ℤ))
⊢ LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)
have 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 ℤ))
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
Cleared hypotheses: H, v_π_lt_one, v_π_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ℤ))
      (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
    (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) 0) : WithZero (Multiplicative ℤ))
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 ℤ))
⊢ LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)
have rwa : 0 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)
Tactic: rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ℤ))
      (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
    (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) 0) : WithZero (Multiplicative ℤ))
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 ℤ))
rwa : 0 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)
⊢ LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)
have rwa₁ : HPow.hPow (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        π :
      WithZero (Multiplicative ℤ))
    (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
  1
Tactic: rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have h_mn : m ≤ n
Tactic: have h_mn : m ≤ n := by
      have v_π_lt_one := (intValuation_lt_one_iff_dvd (maximalIdeal A) π).mpr
          (dvd_of_eq ((irreducible_iff_uniformizer _).mp hπ))
      have v_π_ne_zero : (maximalIdeal A).intValuation π ≠ 0 := intValuation_ne_zero _ _ hπ.ne_zero
      zify
      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
      rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
h_mn : m ≤ n
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have h : (algebraMap A K : (a : A) → K) ((↑u : A) * π ^ (n - m) * w.inv) = x
Tactic: use u * π ^ (n - m) * w.2
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
h_mn : m ≤ n
⊢ (algebraMap A K : (a : A) → K) ((↑u : A) * π ^ (n - m) * w.inv) = x
have h : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑u : A) : K)
    (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
      (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K)) =
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑u : A) : K)
    (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n /
      HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑w : A) : K)
        (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m))
Tactic: simp only [← h_frac, Units.inv_eq_val_inv, _root_.map_mul, _root_.map_pow, map_units_inv,
      mul_assoc, mul_div_assoc ((algebraMap A _) ↑u) _ _]