awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ Membership.mem (γ := Subgroup Γˣ) (zpowers (generator v)) (generator v)

Tactic:
mem_zpowers (IsRankOneDiscrete.generator v)

Premises used: Subgroup.mem_zpowers, Valuation.IsRankOneDiscrete.generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ Membership.mem (γ := Subgroup Γˣ) (zpowers (generator v)) (generator v)

Tactic:
exact mem_zpowers (IsRankOneDiscrete.generator v)

Premises used: Subgroup.mem_zpowers, Valuation.IsRankOneDiscrete.generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ generator v < 1

Tactic:
(exists_generator_lt_one v).choose_spec.2

Premises used: Exists.choose_spec, And.right, Valuation.IsRankOneDiscrete.exists_generator_lt_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ generator v ≠ 1

Tactic:
ne_of_lt <| generator_lt_one v

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, ne_of_lt
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
rw : Units.val '' (↑(valueGroup w) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}
rw₁ rw₂ :
  Eq (α := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0})
    (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0})
⊢ Units.val '' (↑(zpowers (generator w)) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}

Tactic:
rw [generator_zpowers_eq_valueGroup, valueGroup_eq_range]

Premises used: MonoidWithZeroHom.valueGroup_eq_range, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
a : Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}) (↑(generator w) : Γ)
t : Set Γ
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ)) (↑(generator w) : Γ)

Tactic:
apply diff_subset

Premises used: Set.diff_subset
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
⊢ generator w ∈ (↑(zpowers (generator w)) : Set Γˣ) ∧ (↑(generator w) : Γ) = (↑(generator w) : Γ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
⊢ (↑(generator w) : Γ) ∈ Units.val '' (↑(zpowers (generator w)) : Set Γˣ)

Tactic:
exact ⟨generator w, by simp⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ (↑(generator v) : Γ) ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ (ValueGroup₀.embedding : (a : ValueGroup₀ v) → Γ) (↑(generator' v) : WithZero ↥(valueGroup v)) = (↑(generator v) : Γ)

Tactic:
rfl

Premises used: WithZero.recZeroCoe, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
rw : zpowers (↑(generator' v) : Γˣ) = valueGroup v
⊢ Eq (α := Subgroup ↥(valueGroup v)) (zpowers (generator' v)) ⊤

Tactic:
rw [← map_subtype_inj, MonoidHom.map_zpowers,
    subtype_apply, ← MonoidHom.range_eq_map, Subgroup.subtype_range]

Premises used: Subgroup.map_subtype_inj, MonoidHom.range_eq_map, Subgroup.subtype_apply, Subgroup.subtype_range, MonoidHom.map_zpowers
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ zpowers (↑(generator' v) : Γˣ) = valueGroup v

Tactic:
apply generator_zpowers_eq_valueGroup

Premises used: Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ generator' v < 1

Tactic:
(exists_generator_lt_one v).choose_spec.2

Premises used: Exists.choose_spec, And.right, Valuation.IsRankOneDiscrete.exists_generator_lt_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
rw : IsCyclic.{u_1} ↥(zpowers (generator v))
⊢ IsCyclic.{u_1} ↥(valueGroup v)

Tactic:
rw [← generator_zpowers_eq_valueGroup]

Premises used: Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ IsCyclic.{u_1} ↥(zpowers (generator v))

Tactic:
isCyclic_zpowers (generator v)

Premises used: Subgroup.isCyclic_zpowers, Valuation.IsRankOneDiscrete.generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ IsCyclic.{u_1} ↥(zpowers (generator v))

Tactic:
exact isCyclic_zpowers (generator v)

Premises used: Subgroup.isCyclic_zpowers, Valuation.IsRankOneDiscrete.generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
exists_val_nontrivial :
  ∃ (x : A),
    Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ) ∧ Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
⊢ v.IsNontrivial

Tactic:
apply IsNontrivial.mk

Premises used: Valuation.IsNontrivial.mk
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
exists_val_nontrivial :
  ∀
    (h1 :
      ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
        Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)),
    False
⊢ ∃ (x : A),
    Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ) ∧ Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)

Tactic:
by_contra! h1
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
simp : ∀ (y : Γˣ) (x : A) (h : (v : (a : A) → Γ) x = (↑y : Γ)), (↑y : Γ) = (↑1 : Γ)
⊢ Eq (α := Subgroup Γˣ) (valueGroup v) ⊥

Tactic:
simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]

Premises used: Units.ext_iff, Set.mem_range, Set.subset_singleton_iff, forall_exists_index, Subsemigroup.coe_set_mk, MonoidWithZeroHom.valueGroup, Submonoid.coe_set_mk, Subgroup.closure_eq_bot_iff, MonoidWithZeroHom.valueMonoid, Set.mem_preimage
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
y : Γˣ
x : A
⊢ ∀ (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)

Tactic:
specialize h1 x
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
y : Γˣ
x : A
h1 :
  ∀ (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
⊢ ∀ (h : (v : (a : A) → Γ) x = (↑y : Γ)), (↑y : Γ) = (↑1 : Γ)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
⊢ Eq (α := Subgroup Γˣ) (valueGroup v) ⊥

Tactic:
have hvalueGroup : valueGroup v = ⊥ := by
    simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]
    intro y x
    specialize h1 x
    aesop
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
hvalueGroup : Eq (α := Subgroup Γˣ) (valueGroup v) ⊥
⊢ False

Tactic:
aesop (add safe forward [generator_lt_one, generator_zpowers_eq_valueGroup])

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ Subgroup.genLTOne (valueGroup v) = generator v

Tactic:
((valueGroup v).genLTOne_unique (generator_lt_one v) (generator_zpowers_eq_valueGroup v)).symm

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, LinearOrderedCommGroup.Subgroup.genLTOne_unique, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, MonoidWithZeroHom.valueGroup, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
⊢ v.IsUniformizer π ↔ (v : (a : A) → Γ) π = (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
refl _

Premises used: Valuation.IsUniformizer, refl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : π = 0
⊢ 0 = (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
rw [h0, IsUniformizer, map_zero] at hπ

Premises used: Valuation.IsUniformizer, map_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : π = 0
hπ₁ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
⊢ π = 0

Tactic:
rw [h0, IsUniformizer, map_zero] at hπ

Premises used: Valuation.IsUniformizer, map_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
h0 : π = 0
⊢ False

Tactic:
(Units.ne_zero _).symm hπ

Premises used: Units.ne_zero, Ne.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
h0 : π = 0
⊢ False

Tactic:
exact (Units.ne_zero _).symm hπ

Premises used: Units.ne_zero, Ne.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ (v : (a : A) → Γ) π = (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
hπ

Premises used: Valuation.IsUniformizer
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ LT.lt.{u_1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (1 : Γ)

Tactic:
hπ ▸ hv.generator_lt_one

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
by_contra : ∀ (h0 : Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)), False
⊢ Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)

Tactic:
by_contra h0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)
⊢ 0 = (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
simp only [IsUniformizer, h0] at hπ

Premises used: Valuation.IsUniformizer
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
h0 : Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)
hπ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
⊢ False

Tactic:
(Units.ne_zero _).symm hπ

Premises used: Units.ne_zero, Ne.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
h0 : Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)
hπ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
⊢ False

Tactic:
exact (Units.ne_zero _).symm hπ

Premises used: Units.ne_zero, Ne.symm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ (v : (a : A) → Γ) π = (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
rw [IsUniformizer.iff] at hπ

Premises used: Valuation.IsUniformizer.iff
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : (v : (a : A) → Γ) π = (↑(IsRankOneDiscrete.generator v) : Γ)
⊢ LT.lt.{u_1} (α := Γ) (0 : Γ) ((v : (a : A) → Γ) π : Γ)

Tactic:
simp [zero_lt_iff, ne_eq, hπ]

Premises used: ne_eq, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
rw :
  Eq.{u_1 + 1} (α := Subgroup Γˣ) (zpowers (Subgroup.genLTOne (valueGroup v)) : Subgroup Γˣ)
    (zpowers (Units.mk0 ((v : (a : A) → Γ) π) ⋯) : Subgroup Γˣ)
⊢ Eq (α := Subgroup Γˣ) (valueGroup v) (zpowers (Units.mk0 ((v : (a : A) → Γ) π) ⋯))

Tactic:
rw [← (valueGroup v).genLTOne_zpowers_eq_top]

Premises used: MonoidWithZeroHom.valueGroup, LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
e_g : Eq.{u_1 + 1} (α := Γˣ) (Subgroup.genLTOne (valueGroup v) : Γˣ) (Units.mk0 ((v : (a : A) → Γ) π) ⋯ : Γˣ)
⊢ Eq.{u_1 + 1} (α := Subgroup Γˣ) (zpowers (Subgroup.genLTOne (valueGroup v)) : Subgroup Γˣ)
    (zpowers (Units.mk0 ((v : (a : A) → Γ) π) ⋯) : Subgroup Γˣ)

Tactic:
congr
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
e_g : Subgroup.genLTOne (valueGroup v) = IsRankOneDiscrete.generator v
⊢ Eq.{u_1 + 1} (α := Γˣ) (Subgroup.genLTOne (valueGroup v) : Γˣ) (Units.mk0 ((v : (a : A) → Γ) π) ⋯ : Γˣ)

Tactic:
simp only [val, Units.mk0_val, hπ]

Premises used: Valuation.IsUniformizer.val, Units.mk0_val
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Subgroup.genLTOne (valueGroup v) = IsRankOneDiscrete.generator v

Tactic:
IsRankOneDiscrete.valueGroup_genLTOne_eq_generator v

Premises used: Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Subgroup.genLTOne (valueGroup v) = IsRankOneDiscrete.generator v

Tactic:
exact IsRankOneDiscrete.valueGroup_genLTOne_eq_generator v

Premises used: Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
⊢ (↑π.val : A) ≠ 0

Tactic:
π.2.ne_zero

Premises used: Valuation.IsUniformizer.ne_zero, Valuation.Uniformizer.valuation_gt_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : CommRing R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
π : ↥v.integer
hπ : v.IsUniformizer (↑π : R)
⊢ ¬IsUnit π

Tactic:
fun h ↦ ne_of_gt hπ.val_lt_one (Integers.one_of_isUnit (integer.integers v) h).symm

Premises used: Valuation.integer.integers, ne_of_gt, Eq.symm, Valuation.IsUniformizer.val_lt_one, Not, Valuation.Integers.one_of_isUnit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ v.IsRankOneDiscrete

Tactic:
⟨(valueGroup v).genLTOne,
    ⟨(valueGroup v).genLTOne_zpowers_eq_top, (valueGroup v).genLTOne_lt_one⟩⟩

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_lt_one, Valuation.IsRankOneDiscrete.mk, LinearOrderedCommGroup.Subgroup.genLTOne, And.intro, Exists.intro, MonoidWithZeroHom.valueGroup, LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
simp : ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
⊢ ∃ (π : ↥v.valuationSubring), v.IsUniformizer (↑π : K)

Tactic:
simp only [IsUniformizer.iff, Subtype.exists, mem_valuationSubring_iff, exists_prop]

Premises used: Subtype.exists, Valuation.mem_valuationSubring_iff, exists_prop, 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 Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ let g : Γˣ := Subgroup.genLTOne (valueGroup v);
  g = Subgroup.genLTOne (valueGroup v)

Tactic:
set g := (valueGroup v).genLTOne with hg

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne, MonoidWithZeroHom.valueGroup
-- 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)
rw : (↑(Subgroup.genLTOne (valueGroup v)) : Γ) ∈ Units.val '' (↑(valueGroup v) : Set Γˣ)
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ) \ {0}) (↑g : Γ)

Tactic:
rw [← valueGroup_eq_range, hg]

Premises used: MonoidWithZeroHom.valueGroup_eq_range
-- 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)
⊢ (↑(Subgroup.genLTOne (valueGroup v)) : Γ) ∈ Units.val '' (↑(valueGroup v) : Set Γˣ)

Tactic:
exact mem_image_of_mem Units.val (valueGroup v).genLTOne_mem

Premises used: Units.val, Set.mem_image_of_mem, MonoidWithZeroHom.valueGroup, LinearOrderedCommGroup.Subgroup.genLTOne_mem
-- 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)
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) : Γ)
⊢ ∃ (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

Premises used: Units.val, SDiff.sdiff, Set.range, Singleton.singleton, OfNat.ofNat, 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 Γ
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 : Γ)
h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) π : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) π = (↑(generator v) : Γ)
⊢ ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)

Tactic:
use π
-- 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 : Γ)
h :
  LE.le.{u_1} (α := Γ) (↑(Subgroup.genLTOne (valueGroup v)) : Γ) 1 ∧
    (↑(Subgroup.genLTOne (valueGroup v)) : Γ) = (↑(generator v) : Γ)
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) π : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) π = (↑(generator v) : Γ)

Tactic:
rw [hπ, hg]