awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw₁ : HMul.hMul (β := Γ) (HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) (-m)) ((v : (a : K) → Γ) (↑r : K) : Γ) = 1
Tactic: rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw₂ : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) (-m) *
    HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
  1
Tactic: rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw₃ : (HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m)⁻¹ *
    HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
  1
Tactic: rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw₄ : HMul.hMul (α := Γ) (β := Γ) (((v : (a : K) → Γ) (↑r : K))⁻¹ : Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) = 1
Tactic: rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw₅ : Eq.{u_1 + 1} (α := Γ) 1 1
Tactic: rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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 : ℤ)
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hpow : 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₀]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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 : Γ)
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have ha : let a : ↥v.valuationSubring :=
  Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) sorry;
a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) sorry
Tactic: set a : K₀ := ⟨π.1.1 ^ (-m) * r, by apply le_of_eq hpow⟩ with ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
have simp : ¬(↑π.val : K) ^ m = 0 ∧ ¬r = 0
Tactic: simp only [zpow_neg, ne_eq, mul_eq_zero, inv_eq_zero, ZeroMemClass.coe_eq_zero, not_or, ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
have refine : ¬(↑π.val : K) ^ m = 0
Tactic: refine ⟨?_, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
have rw : ¬(↑π.val : K) = 0 ∨ ¬n ≠ 0
Tactic: rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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)) ⋯
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have ha₀ : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have h_unit_a : IsUnit a
Tactic: have h_unit_a : IsUnit a :=
    Integers.isUnit_of_one (integer.integers v) (isUnit_iff_ne_zero.mpr ha₀) hpow
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have h : (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
Tactic: use h_unit_a.unit
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h : (↑r : K) = (↑(π.val ^ n) : K) * (↑a : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₁ : (↑r : K) = (↑π.val : K) ^ n * (↑a : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₃ : (↑r : K) = (↑π.val : K) ^ n * (↑π.val : K) ^ (-m) * (↑r : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₄ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ m)⁻¹ * (↑r : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₅ : (↑r : K) = (↑π.val : K) ^ n * (HPow.hPow (β := ℤ) (↑π.val : K) (↑n : ℤ))⁻¹ * (↑r : 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]