awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
rw : HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m)) : Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) = 1
rw₁ :
  HMul.hMul (β := Γ) (HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) (-m)) ((v : (a : K) → Γ) (↑r : K) : Γ) = 1
rw₂ :
  HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) (-m) *
      HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
    1
rw₃ :
  (HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m)⁻¹ *
      HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
    1
rw₄ : HMul.hMul (α := Γ) (β := Γ) (((v : (a : K) → Γ) (↑r : K))⁻¹ : Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) = 1
rw₅ rw₆ : Eq.{u_1 + 1} (α := Γ) 1 1
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)

Tactic:
rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]

Premises used: map_mul, zpow_neg, map_zpow₀, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)

Tactic:
have hpow : v (π.1.1 ^ (-m) * r) = 1 := by
    rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
⊢ (↑π.val : K) ^ (-m) * (↑r : K) ∈ v.valuationSubring

Tactic:
apply le_of_eq hpow

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
⊢ let a : ↥v.valuationSubring :=
    Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯;
  a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯

Tactic:
set a : K₀ := ⟨π.1.1 ^ (-m) * r, by apply le_of_eq hpow⟩ with ha
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
simp : ¬(↑π.val : K) ^ m = 0 ∧ ¬r = 0
⊢ (↑a : K) ≠ 0

Tactic:
simp only [zpow_neg, ne_eq, mul_eq_zero, inv_eq_zero, ZeroMemClass.coe_eq_zero, not_or, ha]

Premises used: ZeroMemClass.coe_eq_zero, inv_eq_zero, mul_eq_zero, ne_eq, not_or, zpow_neg
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
⊢ ¬(↑π.val : K) ^ m = 0 ∧ ¬r = 0

Tactic:
⟨?_, hr⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
refine : ¬(↑π.val : K) ^ m = 0
⊢ ¬(↑π.val : K) ^ m = 0 ∧ ¬r = 0

Tactic:
refine ⟨?_, hr⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
rw : ¬(↑π.val : K) = 0 ∨ ¬n ≠ 0
⊢ ¬(↑π.val : K) ^ m = 0

Tactic:
rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]

Premises used: zpow_natCast, pow_eq_zero_iff', not_and_or
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
⊢ ¬(↑π.val : K) = 0 ∨ ¬n ≠ 0

Tactic:
Or.inl π.ne_zero

Premises used: Valuation.Uniformizer.ne_zero, Or.inl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
⊢ ¬(↑π.val : K) = 0 ∨ ¬n ≠ 0

Tactic:
exact Or.inl π.ne_zero

Premises used: Valuation.Uniformizer.ne_zero, Or.inl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
⊢ (↑a : K) ≠ 0

Tactic:
have ha₀ : (↑a : K) ≠ 0 := by
    simp only [zpow_neg, ne_eq, mul_eq_zero, inv_eq_zero, ZeroMemClass.coe_eq_zero, not_or, ha]
    refine ⟨?_, hr⟩
    rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]
    exact Or.inl π.ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
⊢ IsUnit a

Tactic:
have h_unit_a : IsUnit a :=
    Integers.isUnit_of_one (integer.integers v) (isUnit_iff_ne_zero.mpr ha₀) hpow
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
h_unit_a : IsUnit a
h : (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)

Tactic:
use h_unit_a.unit

Premises used: IsUnit.unit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
h_unit_a : IsUnit a
h : (↑r : K) = (↑(π.val ^ n) : K) * (↑a : K)
h₁ : (↑r : K) = (↑π.val : K) ^ n * (↑a : K)
h₂ :
  (↑r : K) =
    (↑π.val : K) ^ n *
      (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯) : K)
h₃ : (↑r : K) = (↑π.val : K) ^ n * (↑π.val : K) ^ (-m) * (↑r : K)
h₄ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ m)⁻¹ * (↑r : K)
h₅ : (↑r : K) = (↑π.val : K) ^ n * (HPow.hPow (β := ℤ) (↑π.val : K) (↑n : ℤ))⁻¹ * (↑r : K)
h₆ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ n)⁻¹ * (↑r : K)
h₇ : (↑r : K) = 1 * (↑r : K)
h₈ h₉ : (↑r : K) = (↑r : K)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)

Tactic:
rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]

Premises used: zpow_natCast, mul_inv_cancel₀, mul_assoc, pow_ne_zero, Valuation.Uniformizer.ne_zero, zpow_neg, Subring.coe_pow, IsUnit.unit_spec, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
hJ : Ne (α := Ideal ↥v.valuationSubring) (span {π.val}) ⊤
IJ : LE.le (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π.val})
⊢ Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π.val})

Tactic:
apply (maximalIdeal.isMaximal _).eq_of_le

Premises used: IsLocalRing.maximalIdeal.isMaximal, Ideal.IsMaximal.eq_of_le
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
h : Eq (α := Ideal ↥v.valuationSubring) (span {π.val}) ⊤
⊢ IsUnit π.val

Tactic:
rw [Ideal.span_singleton_eq_top] at h

Premises used: Ideal.span_singleton_eq_top
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
h : IsUnit π.val
⊢ False

Tactic:
apply π.2.not_isUnit h

Premises used: Valuation.IsUniformizer.not_isUnit, Valuation.Uniformizer.valuation_gt_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
pos : ∀ (hx₀ : x = 0), Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
neg : ∀ (hx₀ : ¬x = 0), Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x

Tactic:
by_cases hx₀ : x = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : x = 0
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x

Tactic:
simp [hx₀]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
neg :
  ∀ (n : ℕ) (u : (↥v.valuationSubring)ˣ) (hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
    Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x

Tactic:
obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π

Premises used: Valuation.exists_pow_Uniformizer
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ x = π.val ^ n * (↑u : ↥v.valuationSubring)

Tactic:
rw [← Subring.coe_mul, Subtype.coe_inj] at hu

Premises used: Subtype.coe_inj, Subring.coe_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
⊢ ¬IsUnit x

Tactic:
have hn : Not (IsUnit x) := fun h ↦
        (maximalIdeal.isMaximal _).ne_top (eq_top_of_isUnit_mem _ hx h)
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬IsUnit x
h : n = 0
⊢ False

Tactic:
simp only [hu, h, pow_zero, one_mul, Units.isUnit, not_true] at hn

Premises used: pow_zero, not_true, Units.isUnit, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬IsUnit x
⊢ n ≠ 0

Tactic:
replace hn : n ≠ 0 := fun h ↦ by
        simp only [hu, h, pow_zero, one_mul, Units.isUnit, not_true] at hn
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : n ≠ 0
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x

Tactic:
simp [Ideal.mem_span_singleton, hu, dvd_pow_self _ hn]

Premises used: dvd_pow_self, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
⊢ Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π})

Tactic:
Uniformizer.is_generator ⟨π, hπ⟩

Premises used: Set.Mem, Valuation.Uniformizer.mk, Valuation.integer, Valuation.valuationSubring, Valuation.Uniformizer.is_generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
n : ℕ
rw :
  HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n =
    HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
rw₁ : HPow.hPow (α := Ideal ↥v.valuationSubring) (span {π.val}) n = HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
rw₂ : v.Uniformizer
rw₃ : HPow.hPow (α := Ideal ↥v.valuationSubring) (span {π.val}) n = HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
rw₄ : v.Uniformizer
⊢ HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n = span {π.val ^ n}

Tactic:
rw [← Ideal.span_singleton_pow, Uniformizer.is_generator]

Premises used: Valuation.Uniformizer.is_generator, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
obtain : ∀ (π : ↥v.valuationSubring) (hπ : v.IsUniformizer (↑π : K)), ¬IsField.{u_2} ↥v.valuationSubring
⊢ ¬IsField.{u_2} ↥v.valuationSubring

Tactic:
obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v

Premises used: Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial