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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
g : Γˣ := Subgroup.genLTOne (valueGroup v)
hg : g = Subgroup.genLTOne (valueGroup v)
⊢ ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
have obtain : ∀ (hγ0 : (↑g : Γ) ∉ {0}) (π : K) (hπ : (v : (a : K) → Γ) π = (↑g : Γ)),
  ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
Tactic: obtain ⟨⟨π, hπ⟩, hγ0⟩ : g.1 ∈ ((range v) \ {0}) := by
    rw [← valueGroup_eq_range, hg]
    exact mem_image_of_mem Units.val (valueGroup v).genLTOne_mem
-- 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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
g : Γˣ := Subgroup.genLTOne (valueGroup v)
hg : g = Subgroup.genLTOne (valueGroup v)
hγ0 : (↑g : Γ) ∉ {0}
π : K
hπ : (v : (a : K) → Γ) π = (↑g : Γ)
⊢ ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
have h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) π : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) π = (↑(generator v) : Γ)
Tactic: use π
-- 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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
g : Γˣ := Subgroup.genLTOne (valueGroup v)
hg : g = Subgroup.genLTOne (valueGroup v)
hγ0 : (↑g : Γ) ∉ {0}
π : K
hπ : (v : (a : K) → Γ) π = (↑g : Γ)
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) π : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) π = (↑(generator v) : Γ)
have h : LE.le.{u_1} (α := Γ) (↑(Subgroup.genLTOne (valueGroup v)) : Γ) 1 ∧
  (↑(Subgroup.genLTOne (valueGroup v)) : Γ) = (↑(generator v) : Γ)
Tactic: rw [hπ, hg]
-- 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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
g : Γˣ := Subgroup.genLTOne (valueGroup v)
hg : g = Subgroup.genLTOne (valueGroup v)
hγ0 : (↑g : Γ) ∉ {0}
π : K
hπ : (v : (a : K) → Γ) π = (↑g : Γ)
⊢ (↑(Subgroup.genLTOne (valueGroup v)) : Γ) = (↑(generator v) : Γ)
have rw : (↑(generator v) : Γ) = (↑(generator v) : Γ)
Tactic: rw [valueGroup_genLTOne_eq_generator]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
H : Associated π₁ π₂
⊢ v.IsUniformizer (↑π₂ : K)
have obtain : ∀ (u : (↥v.valuationSubring)ˣ) (hu : π₁ * (↑u : ↥v.valuationSubring) = π₂), v.IsUniformizer (↑π₂ : K)
Tactic: obtain ⟨u, hu⟩ := H
Cleared hypotheses: H
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
⊢ v.IsUniformizer (↑π₂ : K)
have this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
Tactic: have : v (u.1 : K) = 1 := (Integers.isUnit_iff_valuation_eq_one <| integer.integers v).mp u.isUnit
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa₁ : (v : (a : K) → Γ) (↑(π₁ * (↑u : ↥v.valuationSubring)) : K) = (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
rwa₁ : (v : (a : K) → Γ) (↑(π₁ * (↑u : ↥v.valuationSubring)) : K) = (↑(generator v) : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa₂ : (v : (a : K) → Γ) ((↑π₁ : K) * (↑(↑u : ↥v.valuationSubring) : K)) = (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
rwa₁ : (v : (a : K) → Γ) (↑(π₁ * (↑u : ↥v.valuationSubring)) : K) = (↑(generator v) : Γ)
rwa₂ : (v : (a : K) → Γ) ((↑π₁ : K) * (↑(↑u : ↥v.valuationSubring) : K)) = (↑(generator v) : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa₃ : HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) (↑π₁ : K) : Γ)
    ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) =
  (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
rwa₁ : (v : (a : K) → Γ) (↑(π₁ * (↑u : ↥v.valuationSubring)) : K) = (↑(generator v) : Γ)
rwa₂ : (v : (a : K) → Γ) ((↑π₁ : K) * (↑(↑u : ↥v.valuationSubring) : K)) = (↑(generator v) : Γ)
rwa₃ :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) (↑π₁ : K) : Γ)
      ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) =
    (↑(generator v) : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa₄ : HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) (↑π₁ : K) : Γ) (1 : Γ) = (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
this : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) (1 : Γ)
rwa : (v : (a : K) → Γ) (↑π₂ : K) = (↑(generator v) : Γ)
rwa₁ : (v : (a : K) → Γ) (↑(π₁ * (↑u : ↥v.valuationSubring)) : K) = (↑(generator v) : Γ)
rwa₂ : (v : (a : K) → Γ) ((↑π₁ : K) * (↑(↑u : ↥v.valuationSubring) : K)) = (↑(generator v) : Γ)
rwa₃ :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) (↑π₁ : K) : Γ)
      ((v : (a : K) → Γ) (↑(↑u : ↥v.valuationSubring) : K) : Γ) =
    (↑(generator v) : Γ)
rwa₄ : HMul.hMul (α := Γ) (β := Γ) ((v : (a : K) → Γ) (↑π₁ : K) : Γ) (1 : Γ) = (↑(generator v) : Γ)
⊢ v.IsUniformizer (↑π₂ : K)
have rwa₅ : (v : (a : K) → Γ) (↑π₁ : K) = (↑(generator v) : Γ)
Tactic: rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
⊢ Associated π₁ π₂
have hval : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)
Tactic: have hval : v ((π₁ : K)⁻¹ * π₂) = 1 := by
    simp [IsUniformizer.iff.mp h1, IsUniformizer.iff.mp h2]
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
hval : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)
⊢ Associated π₁ π₂
have hp : let p := Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) sorry;
p = Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) sorry
Tactic: set p : v.integer := ⟨(π₁.1 : K)⁻¹ * π₂.1, (v.mem_integer_iff _).mpr (le_of_eq hval)⟩ with hp
-- 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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
hval : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)
p : ↥v.integer := Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯
hp : p = Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯
⊢ Associated π₁ π₂
have h : π₁ * (↑(IsUnit.unit (a := p) sorry) : ↥v.valuationSubring) = π₂
Tactic: use ((Integers.isUnit_iff_valuation_eq_one (x := p) <| integer.integers v).mpr hval).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
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
hval : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)
p : ↥v.integer := Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯
hp : p = Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯
⊢ π₁ * (↑(IsUnit.unit (a := p) ⋯) : ↥v.valuationSubring) = π₂
have h : (↑(π₁ * (↑(IsUnit.unit (a := p) sorry) : ↥v.valuationSubring)) : K) = (↑π₂ : K)
Tactic: apply_fun ((↑) : K₀ → K) using Subtype.val_injective
-- 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
⊢ Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
have rw : ¬r = 0
Tactic: rw [ne_eq, zero_iff, Subring.coe_eq_zero_iff]
-- 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
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
Tactic: have hr₀ : v r ≠ 0 := by rw [ne_eq, zero_iff, Subring.coe_eq_zero_iff]; exact 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 : Γ)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hvr_def : let vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀;
vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
Tactic: set vr : Γˣ := Units.mk0 (v r) hr₀ with hvr_def
-- 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₀
⊢ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) vr
have hb : Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ)) (↑vr : Γ)
Tactic: apply mem_valueGroup
-- 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₀
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ)) (↑vr : Γ)
have hb : Membership.mem.{u_1, u_1} (α := Γ) (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ))
  ((v : (a : K) → Γ) (↑r : K) : Γ)
Tactic: rw [hvr_def, Units.val_mk0 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₀
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hvr : Membership.mem (γ := Subgroup Γˣ) (valueGroup v) vr
Tactic: have hvr : vr ∈ (valueGroup v) := by
    apply mem_valueGroup
    rw [hvr_def, Units.val_mk0 hr₀]
    exact mem_range_self _
-- 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₀
hvr : Membership.mem (γ := Subgroup Γˣ) (valueGroup v) vr
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hvr₁ : ∃ (k : ℤ), HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) sorry : Γˣ) k = vr
Tactic: rw [π.2.zpowers_eq_valueGroup, mem_zpowers_iff] at hvr
Cleared hypotheses: hvr
-- 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₀
hvr : ∃ (k : ℤ), HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) k = vr
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have obtain : ∀ (m : ℤ) (hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) sorry : Γˣ) m = vr),
  ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
Tactic: obtain ⟨m, hm⟩ := hvr
Cleared hypotheses: hvr
-- 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 = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
⊢ HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
have rw : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
  (↑(HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) sorry : Γˣ) m) : Γ)
Tactic: rw [← Units.val_mk0 hr₀, ← hm]
-- 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
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
Tactic: have hm' : v π.val ^ m = v r := by
    rw [hvr_def] at hm
    rw [← Units.val_mk0 hr₀, ← hm]
    simp [Units.val_zpow_eq_zpow_val, Units.val_mk0]
-- 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)
⊢ 0 ≤ m
have rw : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (1 : Γ)
Tactic: rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']
-- 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)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have hm₀ : 0 ≤ m
Tactic: have hm₀ : 0 ≤ m := by
    rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']
    exact r.2
-- 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 : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have obtain : ∀ (n : ℕ) (hn : m = (↑n : ℤ)),
  ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
Tactic: obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hm₀
-- 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 : ℤ)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
have h : ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
Tactic: use n
-- 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 : ℤ)
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
have rw : HMul.hMul (α := Γ) (β := Γ) ((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₀]