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 Γ
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 : Γ)
rw rw₁ : (↑(generator v) : Γ) = (↑(generator v) : Γ)
⊢ (↑(Subgroup.genLTOne (valueGroup v)) : Γ) = (↑(generator v) : Γ)

Tactic:
rw [valueGroup_genLTOne_eq_generator]

Premises used: Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator
-- 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 : 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} (α := Γ) (↑(Subgroup.genLTOne (valueGroup v)) : Γ) 1 ∧
    (↑(Subgroup.genLTOne (valueGroup v)) : Γ) = (↑(generator v) : Γ)

Tactic:
exact ⟨le_of_lt (valueGroup v).genLTOne_lt_one, by rw [valueGroup_genLTOne_eq_generator]⟩
-- 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 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ Nonempty.{u_2 + 1} v.Uniformizer

Tactic:
⟨⟨(exists_isUniformizer_of_isCyclic_of_nontrivial v).choose,
    (exists_isUniformizer_of_isCyclic_of_nontrivial v).choose_spec⟩⟩

Premises used: Exists.choose_spec, Valuation.Uniformizer.mk, Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial, Nonempty.intro, Exists.choose
-- 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
h1 : v.IsUniformizer (↑π₁ : K)
H : Associated π₁ π₂
obtain : ∀ (u : (↥v.valuationSubring)ˣ) (hu : π₁ * (↑u : ↥v.valuationSubring) = π₂), v.IsUniformizer (↑π₂ : K)
⊢ v.IsUniformizer (↑π₂ : K)

Tactic:
obtain ⟨u, hu⟩ := 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.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
u : (↥v.valuationSubring)ˣ
hu : π₁ * (↑u : ↥v.valuationSubring) = π₂
⊢ 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
-- 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
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) : Γ)
rwa₅ : (v : (a : K) → Γ) (↑π₁ : K) = (↑(generator v) : Γ)
rwa₆ rwa₇ rwa₈ rwa₉ : v.IsUniformizer (↑π₁ : K)
⊢ v.IsUniformizer (↑π₂ : K)

Tactic:
rwa [IsUniformizer.iff, ← hu, Subring.coe_mul, map_mul, this, mul_one, ← IsUniformizer.iff]

Premises used: Subring.coe_mul, map_mul, Valuation.IsUniformizer.iff, mul_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.valuationSubring
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
⊢ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)

Tactic:
simp [IsUniformizer.iff.mp h1, IsUniformizer.iff.mp h2]

Premises used: Iff.mp, Valuation.IsUniformizer.iff
-- 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
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
⊢ 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]
-- 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
h1 : v.IsUniformizer (↑π₁ : K)
h2 : v.IsUniformizer (↑π₂ : K)
hval : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) : Γ) (1 : Γ)
⊢ let p := Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯;
  p = Subtype.mk (p := fun (x : K) ↦ x ∈ v.integer) ((↑π₁ : K)⁻¹ * (↑π₂ : K)) ⋯

Tactic:
set p : v.integer := ⟨(π₁.1 : K)⁻¹ * π₂.1, (v.mem_integer_iff _).mpr (le_of_eq hval)⟩ with hp

Premises used: Valuation.integer
-- 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
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)) ⋯
h : π₁ * (↑(IsUnit.unit (a := p) ⋯) : ↥v.valuationSubring) = π₂
⊢ Associated π₁ π₂

Tactic:
use ((Integers.isUnit_iff_valuation_eq_one (x := p) <| integer.integers v).mpr hval).unit

Premises used: Iff.mpr, Valuation.integer.integers, IsUnit.unit, Valuation.Integers.isUnit_iff_valuation_eq_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.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)) ⋯
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := ↥v.valuationSubring)
    (Subtype.val (p := fun (x : K) ↦ x ∈ v.valuationSubring))

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
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)) ⋯
h : (↑(π₁ * (↑(IsUnit.unit (a := p) ⋯) : ↥v.valuationSubring)) : K) = (↑π₂ : K)
⊢ π₁ * (↑(IsUnit.unit (a := p) ⋯) : ↥v.valuationSubring) = π₂

Tactic:
apply_fun ((↑) : K₀ → K) using Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
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)) : K) = (↑π₂ : K)

Tactic:
simp [hp, ← mul_assoc, mul_inv_cancel₀ h1.ne_zero]

Premises used: mul_inv_cancel₀, mul_assoc, Valuation.IsUniformizer.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
rw : ¬r = 0
⊢ Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)

Tactic:
rw [ne_eq, zero_iff, Subring.coe_eq_zero_iff]

Premises used: Valuation.zero_iff, ne_eq, Subring.coe_eq_zero_iff
-- 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
⊢ ¬r = 0

Tactic:
hr

Premises used: Set.Mem
-- 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
⊢ ¬r = 0

Tactic:
exact 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
⊢ 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
-- 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 : Γ)
⊢ 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

Premises used: Units.mk0, Subtype.val, DFunLike.coe
-- 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₀
hb : Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ)) (↑vr : Γ)
⊢ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) vr

Tactic:
apply mem_valueGroup

Premises used: MonoidWithZeroHom.mem_valueGroup
-- 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₀
hb :
  Membership.mem.{u_1, u_1} (α := Γ) (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ))
    ((v : (a : K) → Γ) (↑r : K) : Γ)
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ)) (↑vr : Γ)

Tactic:
rw [hvr_def, Units.val_mk0 hr₀]

Premises used: Units.val_mk0
-- 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₀
⊢ Membership.mem.{u_1, u_1} (α := Γ) (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ))
    ((v : (a : K) → Γ) (↑r : K) : Γ)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem
-- 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₀
⊢ Membership.mem.{u_1, u_1} (α := Γ) (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ))
    ((v : (a : K) → Γ) (↑r : K) : Γ)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- 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₀
⊢ 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 _
-- 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₀
hvr : Membership.mem (γ := Subgroup Γˣ) (valueGroup v) vr
⊢ ∃ (k : ℤ), HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) k = vr

Tactic:
rw [π.2.zpowers_eq_valueGroup, mem_zpowers_iff] at hvr

Premises used: Valuation.IsUniformizer.zpowers_eq_valueGroup, Subgroup.mem_zpowers_iff, 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
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
obtain :
  ∀ (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)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)

Tactic:
obtain ⟨m, hm⟩ := hvr
-- 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
⊢ HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀

Tactic:
rw [hvr_def] at hm
-- 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 = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
rw :
  HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
    (↑(HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m) : Γ)
⊢ HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)

Tactic:
rw [← Units.val_mk0 hr₀, ← hm]

Premises used: Units.val_mk0
-- 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 = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
⊢ HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m =
    (↑(HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m) : Γ)

Tactic:
simp [Units.val_zpow_eq_zpow_val, Units.val_mk0]

Premises used: Units.val_zpow_eq_zpow_val, Units.val_mk0
-- 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
⊢ 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]
-- 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)
rw : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (1 : Γ)
⊢ 0 ≤ m

Tactic:
rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']

Premises used: zpow_le_one_iff_right_of_lt_one₀, Valuation.IsUniformizer.val_pos, Valuation.IsUniformizer.val_lt_one, 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
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)
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (1 : Γ)

Tactic:
r.2

Premises used: Set.Mem, setOf, Subtype.property
-- 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)
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (1 : Γ)

Tactic:
exact r.2

Premises used: Subtype.property
-- 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)
⊢ 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
-- 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
obtain :
  ∀ (n : ℕ) (hn : m = (↑n : ℤ)),
    ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)

Tactic:
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hm₀

Premises used: Int.eq_ofNat_of_zero_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
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 : ℤ)
h : ∃ (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ ∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)

Tactic:
use n