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
π : 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 ℤ))
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:
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 ℤ))
      (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 : ℤ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ)) ≤
    1
⊢ LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ)

Tactic:
rwa [← sub_nonneg, ← zpow_le_one_iff_right_of_lt_one₀ (zero_lt_iff.mpr v_π_ne_zero)
        v_π_lt_one]

Premises used: Iff.mpr, zpow_le_one_iff_right_of_lt_one₀, zero_lt_iff, sub_nonneg
-- 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
⊢ 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]
-- 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
h_mn : m ≤ n
h : (algebraMap A K : (a : A) → K) ((↑u : A) * π ^ (n - m) * w.inv) = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
use u * π ^ (n - m) * w.2

Premises used: HSub.hSub, Units.inv
-- 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
h_mn : m ≤ n
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))
⊢ (algebraMap A K : (a : A) → K) ((↑u : A) * π ^ (n - m) * w.inv) = x

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) _ _]

Premises used: Units.val, Algebra.algebraMap, Units.inv_eq_val_inv, mul_assoc, mul_div_assoc, map_pow, map_units_inv, map_mul, DFunLike.coe
-- 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
h_mn : m ≤ n
h :
  HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
      (((algebraMap A K : (a : A) → K) (↑w : 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)
⊢ 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:
congr 1
-- 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
h_mn : m ≤ n
h :
  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)
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
        (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹)
      (((algebraMap A K : (a : A) → K) (↑w : 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) =
    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:
rw [div_eq_mul_inv, mul_inv, mul_comm ((algebraMap A _) ↑w)⁻¹ _, ←
      mul_assoc _ _ ((algebraMap A _) ↑w)⁻¹]

Premises used: Units.val, Algebra.algebraMap, mul_inv, mul_assoc, div_eq_mul_inv, Inv.inv, mul_comm, DFunLike.coe
-- 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
h_mn : m ≤ n
h :
  HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m) =
    HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹
⊢ 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)
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
        (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹)
      (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K)

Tactic:
congr
-- 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
h_mn : m ≤ n
rw : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) π : K) (0 : K)
⊢ HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m) =
    HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹

Tactic:
rw [pow_sub₀ _ _ h_mn]

Premises used: pow_sub₀
-- 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
h_mn : m ≤ n
hx : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) π
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) π : K) (0 : K)

Tactic:
apply IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors

Premises used: IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
-- 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
h_mn : m ≤ n
hx : π ≠ 0
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) π

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_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
h_mn : m ≤ n
⊢ π ≠ 0

Tactic:
hπ.ne_zero

Premises used: Irreducible.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
h_mn : m ≤ n
⊢ π ≠ 0

Tactic:
exact hπ.ne_zero

Premises used: Irreducible.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
h :
  ∀ (a : K),
    Membership.mem (γ := Submonoid K)
        (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) a ↔
      Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) a
⊢ Eq (α := Submonoid K) (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
    (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A))

Tactic:
ext a
-- 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
a : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro