awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
this : Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) (y / x)
⊢ ∃ (u : Aˣ), u • x = y
have neg : ∀ (u : A) (h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x), ∃ (u : Aˣ), u • x = y
Tactic: obtain ⟨u, h⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h_1 :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x
⊢ ∃ (u : Aˣ), u • x = y
have h₁ : IsUnit.unit sorry • x = y
Tactic: use IsUnit.unit h.1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h_1 :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x
⊢ IsUnit.unit ⋯ • x = y
have h₁ : y / x * x = y
Tactic: simp only [Units.smul_def, Algebra.smul_def, IsUnit.unit_spec, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ Eq (α := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
    (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
have h : ∀ (x : K),
  Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
have h : ∀ (h : Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x),
  Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h :
  ∀ (h : Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x),
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
have h₁ : ∀
  (h :
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x),
  Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x
⊢ Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
have h₁ : ∀ (w : A),
  Membership.mem (γ := Subring A) ⊤ w →
    ∀
      (h :
        Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
          (((algebraMap A K : A →+* K) : (a : A) → K) w : K)),
      Membership.mem (α := K) (γ := Subring K)
        (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
        (((algebraMap A K : A →+* K) : (a : A) → K) w : K)
Tactic: obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x
have h₁ : ∀ (y : A)
  (h :
    Membership.mem (α := K) (γ := Subring K)
      (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
      ((algebraMap A K : (a : A) → K) y : K)),
  Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
    ((algebraMap A K : (a : A) → K) y : K)
Tactic: obtain ⟨y, rfl⟩ := exists_lift_of_le_one h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
⊢ 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 ℤ))
have 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 ℤ))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ℤ))
have 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 ℤ))
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible A
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
x : A
hx : ¬x = 0
ϖ : 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 ℤ))
have 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 ℤ))
Tactic: obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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) * ϖ ^ 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 ℤ))
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
⊢ (valueGroup₀_equiv_withZeroMulInt v : (a : ValueGroup₀ v) → WithZero (Multiplicative ℤ))
      ((↑(generator' v) : WithZero ↥(valueGroup v)) ^ k) =
    exp (-k)
have simp : HPow.hPow (α := WithZero (Multiplicative ℤ))
    ((↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ) (generator' v)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    k =
  exp (-k)
Tactic: simp only [map_zpow₀, valueGroup₀_equiv_withZeroMulInt_apply, WithZero.map'_coe,
    MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst_1 : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
⊢ HPow.hPow (α := WithZero (Multiplicative ℤ))
      ((↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
              (generator' v)) :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
      k =
    exp (-k)
have rw : Eq (α := Multiplicative ℤ)
  (((intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ) (generator' v ^ k) :
    Multiplicative ℤ)
  ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-k) : Multiplicative ℤ)
Tactic: rw [← WithZero.coe_zpow, WithZero.exp, WithZero.coe_inj, ← map_zpow]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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
⊢ 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 ℤ))
have simp : LT.lt (α := WithZero (Multiplicative ℤ))
  (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
        (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
      x :
    WithZero (Multiplicative ℤ))
  (((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          WithZero ↥(valueGroup v) →*₀ WithZero (Multiplicative ℤ)) :
        (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
      y :
    WithZero (Multiplicative ℤ))
Tactic: simp only [valueGroup₀_equiv_withZeroMulInt, MulEquiv.withZero_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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))
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1
have rw : Subgroup.genLTOne (valueGroup v) = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1
Tactic: rw [← Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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))
⊢ Subgroup.genLTOne (valueGroup v) = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1
have suffices : Units.mk0 (exp (-1)) sorry = Subgroup.genLTOne (valueGroup v)
Tactic: suffices Units.mk0 (exp (-1)) (by simp) = (Subgroup.genLTOne (valueGroup v)) by simp [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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))
⊢ Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (valueGroup v)
have hg : LT.lt (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp (-1)) sorry) 1
Tactic: apply LinearOrderedCommGroup.Subgroup.genLTOne_unique
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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
⊢ Units.mk0 (exp (-1)) ⋯ = Subgroup.genLTOne (valueGroup v)
have hH : Subgroup.zpowers (Units.mk0 (exp (-1)) sorry) = valueGroup v
Tactic: apply LinearOrderedCommGroup.Subgroup.genLTOne_unique
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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))
⊢ Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯) = valueGroup v
have hH : ∀ (n : (WithZero (Multiplicative ℤ))ˣ),
  Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (Subgroup.zpowers (Units.mk0 (exp (-1)) sorry)) n ↔
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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 ℤ))ˣ
⊢ Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (Subgroup.zpowers (Units.mk0 (exp (-1)) ⋯)) n ↔
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) n
have 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)⁻¹ sorry) 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: simp_all only [Int.reduceNeg, exp_neg, Subgroup.mem_zpowers_iff, mem_valueGroup_iff_of_comm,
      ne_eq]
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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)⁻¹
⊢ (∃ (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
have hH : (∃ (k : ℤ), HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) k = n) →
  ∀ (k : ℤ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) 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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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
⊢ ∃ (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
have 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)⁻¹ sorry) k) : WithZero (Multiplicative ℤ)) =
        (v : (a : R) → WithZero (Multiplicative ℤ)) x
Tactic: rw [← h]