awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
pos :
  ∀ (hx : x = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
      ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
        WithZero (Multiplicative ℤ))
neg :
  ∀ (hx : ¬x = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
      ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
hx : x = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
neg :
  ∀ (ϖ : A) (hϖ : Irreducible ϖ),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
      ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible A

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
ϖ : A
hϖ : Irreducible ϖ
neg :
  ∀ (n : ℕ) (u : Aˣ) (hx : ¬(↑u : A) * ϖ ^ n = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
            (a : A) → WithZero (Multiplicative ℤ))
          ((↑u : A) * ϖ ^ n) :
        WithZero (Multiplicative ℤ))
      ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) ((↑u : A) * ϖ ^ n)))⁻¹ :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) x))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬(↑u : A) * ϖ ^ n = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        (↑u : A) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [maximalIdeal]

Premises used: IsDiscreteValuationRing.maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬(↑u : A) * ϖ ^ n = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        (↑u : A) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
have : (maximalIdeal A).intValuation ↑u = 1 := by simp [maximalIdeal]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
ϖ : A
hϖ : Irreducible ϖ
n : ℕ
u : Aˣ
hx : ¬(↑u : A) * ϖ ^ n = 0
this :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        (↑u : A) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
          (a : A) → WithZero (Multiplicative ℤ))
        ((↑u : A) * ϖ ^ n) :
      WithZero (Multiplicative ℤ))
    ((ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦ (↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (((addVal A : AddValuation A ℕ∞) : (a : A) → ℕ∞) ((↑u : A) * ϖ ^ n)))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
simp [(maximalIdeal A).intValuation_singleton hϖ.ne_zero
    hϖ.maximalIdeal_eq, hϖ, this, WithZero.exp_eq_coe_ofAdd (n : ℤ)]

Premises used: WithZero.exp_eq_coe_ofAdd, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, IsDiscreteValuationRing.maximalIdeal, Nat.cast, Irreducible.maximalIdeal_eq, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((valueGroup₀_equiv_withZeroMulInt v : (a : ValueGroup₀ v) → WithZero (Multiplicative ℤ)) 0 :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
simp :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      ((↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
              (generator' v)) :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
      k =
    exp (-k)
⊢ (valueGroup₀_equiv_withZeroMulInt v : (a : ValueGroup₀ v) → WithZero (Multiplicative ℤ))
      ((↑(generator' v) : WithZero ↥(valueGroup v)) ^ k) =
    exp (-k)

Tactic:
simp only [map_zpow₀, valueGroup₀_equiv_withZeroMulInt_apply, WithZero.map'_coe,
    MonoidHom.coe_coe]

Premises used: WithZero.map'_coe, MonoidHom.coe_coe, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, map_zpow₀
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
rw :
  Eq (α := Multiplicative ℤ)
    (((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ) (generator' v ^ k) :
      Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-k) : Multiplicative ℤ)
⊢ HPow.hPow (α := WithZero (Multiplicative ℤ))
      ((↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
              (generator' v)) :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
      k =
    exp (-k)

Tactic:
rw [← WithZero.coe_zpow, WithZero.exp, WithZero.coe_inj, ← map_zpow]

Premises used: WithZero.coe_inj, WithZero.coe_zpow, map_zpow, WithZero.exp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
⊢ Eq (α := Multiplicative ℤ)
    (((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ) (generator' v ^ k) :
      Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-k) : Multiplicative ℤ)

Tactic:
simp [← mulintEquivOfZPowersEqTop_symm_apply_zpow
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)]

Premises used: mulintEquivOfZPowersEqTop_symm_apply_zpow
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : ValueGroup₀ v
hxy : x < y
simp :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
            WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
            WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((valueGroup₀_equiv_withZeroMulInt v : (a : ValueGroup₀ v) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((valueGroup₀_equiv_withZeroMulInt v : (a : ValueGroup₀ v) → WithZero (Multiplicative ℤ)) y :
      WithZero (Multiplicative ℤ))

Tactic:
simp only [valueGroup₀_equiv_withZeroMulInt, MulEquiv.withZero_apply_apply]

Premises used: Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt, MulEquiv.withZero_apply_apply
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : ValueGroup₀ v
hxy : x < y
rwa rwa₁ rwa₂ rwa₃ : x < y
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
            WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
            WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))

Tactic:
rwa [(WithZero.map'_strictMono (MulEquiv.strictMono_symm (mulintEquivOfZPowersEqTop_strictMono
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)
    (Left.one_lt_inv_iff.mpr hv.generator'_lt_one)))).lt_iff_lt]

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
⊢ Ne (α := WithZero (Multiplicative ℤ)) (exp (-1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
rw : Subgroup.genLTOne (valueGroup v) = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
rw [← Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator]

Premises used: Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
⊢ Ne (α := WithZero (Multiplicative ℤ)) (exp (-1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
this : Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (valueGroup v)
⊢ Subgroup.genLTOne (valueGroup v) = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
simp [← this]
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
suffices : Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (valueGroup v)
⊢ Subgroup.genLTOne (valueGroup v) = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
suffices Units.mk0 (exp (-1)) (by simp) = (Subgroup.genLTOne (valueGroup v)) by simp [← this]
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
hg : LT.lt (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp (-1)) ⋯) 1
hH : Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯) = valueGroup v
⊢ Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (valueGroup v)

Tactic:
apply LinearOrderedCommGroup.Subgroup.genLTOne_unique

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_unique
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
⊢ LT.lt (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp (-1)) ⋯) 1

Tactic:
compareOfLessAndEq_eq_lt.mp rfl

Premises used: compareOfLessAndEq_eq_lt, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
⊢ LT.lt (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp (-1)) ⋯) 1

Tactic:
exact compareOfLessAndEq_eq_lt.mp rfl

Premises used: compareOfLessAndEq_eq_lt, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
hH :
  ∀ (n : (WithZero (Multiplicative ℤ))ˣ),
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯)) n ↔
      Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) n
⊢ Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯) = valueGroup v

Tactic:
ext n
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))
n : (WithZero (Multiplicative ℤ))ˣ
hH :
  ∀
    (hπ :
      Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
        (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp 1)⁻¹),
    (∃ (k : ℤ), HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n) ↔
      ∃ (a : R),
        ¬Eq (α := WithZero (Multiplicative ℤ))
              ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
              (0 : WithZero (Multiplicative ℤ)) ∧
          ∃ (x : R),
            HMul.hMul (α := WithZero (Multiplicative ℤ))
                ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
                (↑n : WithZero (Multiplicative ℤ)) =
              (v : (a : R) → WithZero (Multiplicative ℤ)) x
⊢ Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯)) n ↔
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) n

Tactic:
simp_all only [Int.reduceNeg, exp_neg, Subgroup.mem_zpowers_iff, mem_valueGroup_iff_of_comm,
      ne_eq]

Premises used: Int.reduceNeg, ne_eq, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, Subgroup.mem_zpowers_iff, WithZero.exp_neg
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp 1)⁻¹
h :
  ∃ (a : R),
    ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ)) ∧
      ∃ (x : R),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
⊢ HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (-(↑n : WithZero (Multiplicative ℤ)).log) = n

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp 1)⁻¹
hH :
  (∃ (k : ℤ), HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n) →
    ∀ (k : ℤ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n),
      ∃ (a : R),
        ¬Eq (α := WithZero (Multiplicative ℤ))
              ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
              (0 : WithZero (Multiplicative ℤ)) ∧
          ∃ (x : R),
            HMul.hMul (α := WithZero (Multiplicative ℤ))
                ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
                (↑n : WithZero (Multiplicative ℤ)) =
              (v : (a : R) → WithZero (Multiplicative ℤ)) x
⊢ (∃ (k : ℤ), HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n) ↔
    ∃ (a : R),
      ¬Eq (α := WithZero (Multiplicative ℤ))
            ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
            (0 : WithZero (Multiplicative ℤ)) ∧
        ∃ (x : R),
          HMul.hMul (α := WithZero (Multiplicative ℤ))
              ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
              (↑n : WithZero (Multiplicative ℤ)) =
            (v : (a : R) → WithZero (Multiplicative ℤ)) x

Tactic:
refine ⟨fun ⟨k, h⟩ ↦ ?_ , fun _ ↦ ⟨-WithZero.log n, by aesop⟩⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n : (WithZero (Multiplicative ℤ))ˣ
hπ :
  Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp 1)⁻¹
h_1 : ∃ (k : ℤ), HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n
k : ℤ
h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k = n
hH :
  ∃ (a : R),
    ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ)) ∧
      ∃ (x : R),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
            (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
⊢ ∃ (a : R),
    ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
          (0 : WithZero (Multiplicative ℤ)) ∧
      ∃ (x : R),
        HMul.hMul (α := WithZero (Multiplicative ℤ))
            ((v : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
            (↑n : WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x

Tactic:
rw [← h]