awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℤ))
            (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH : ∀ (π : R)
  (hπ :
    Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))),
  ∃ (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: have ⟨π, hπ⟩ := 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_1 : (WithZero (Multiplicative ℤ))ˣ
hπ_1 :
  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_1
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
n : ℕ
h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n) = n_1
⊢ ∃ (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)⁻¹ ⋯) (Int.ofNat n)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH : ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
Tactic: refine ⟨1, ?_, π ^ 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
n_1 : (WithZero (Multiplicative ℤ))ˣ
hπ_1 :
  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_1
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
n : ℕ
h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n) = n_1
hH :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ ∃ (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)⁻¹ ⋯) (Int.ofNat n)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH₁ : HMul.hMul (α := WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
    (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.ofNat n)) :
      WithZero (Multiplicative ℤ)) =
  (v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ n)
Tactic: refine ⟨1, ?_, π ^ 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
n_1 : (WithZero (Multiplicative ℤ))ˣ
hπ_1 :
  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_1
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
n : ℕ
h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.negSucc n) = n_1
⊢ ∃ (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)⁻¹ ⋯) (Int.negSucc n)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH : ¬Eq (α := WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
Tactic: refine ⟨π ^ (n + 1), ?_, 1, ?_⟩
-- 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_1 : (WithZero (Multiplicative ℤ))ˣ
hπ_1 :
  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_1
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
n : ℕ
h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.negSucc n) = n_1
hH :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ ∃ (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)⁻¹ ⋯) (Int.negSucc n)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH₁ : HMul.hMul (α := WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
    (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.negSucc n)) :
      WithZero (Multiplicative ℤ)) =
  (v : (a : R) → WithZero (Multiplicative ℤ)) 1
Tactic: refine ⟨π ^ (n + 1), ?_, 1, ?_⟩
-- 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π_1 :
  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
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
⊢ ∃ (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
have hH : ∀ (n_1 : ℕ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.ofNat n_1) = 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 ℤ))
            (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.ofNat n_1)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
Tactic: cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]
Cleared hypotheses: k, 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π_1 :
  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
π : R
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((exp 1)⁻¹ : WithZero (Multiplicative ℤ))
hH :
  ∀ (n_1 : ℕ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n_1) = 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 ℤ))
              (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n_1)) :
                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 ℤ))
            (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) k) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
have hH₁ : ∀ (n_1 : ℕ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.negSucc n_1) = 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 ℤ))
            (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ sorry) (Int.negSucc n_1)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x
Tactic: cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]
Cleared hypotheses: k, 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        (if h :
            Eq (α := WithZero (Multiplicative ℤ))
              ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
              (0 : WithZero (Multiplicative ℤ)) then
          0
        else
          (↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
have pos : ∀
  (h0 :
    Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))),
  Eq (α := WithZero (Multiplicative ℤ))
    ((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        0 :
      WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
Tactic: split_ifs with h0
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
pos :
  ∀
    (h0 :
      Eq (α := WithZero (Multiplicative ℤ))
        ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
    Eq (α := WithZero (Multiplicative ℤ))
      ((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
            (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        (if h :
            Eq (α := WithZero (Multiplicative ℤ))
              ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
              (0 : WithZero (Multiplicative ℤ)) then
          0
        else
          (↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
have neg : ∀
  (h0 :
    ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
  Eq (α := WithZero (Multiplicative ℤ))
    ((map' (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : ↥(valueGroup v) →* Multiplicative ℤ) :
          (a : WithZero ↥(valueGroup v)) → WithZero (Multiplicative ℤ))
        ((↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) sorry) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) :
      WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
Tactic: split_ifs with h0
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
| (v : (a : R) → WithZero (Multiplicative ℤ)) x
have rw : (↑(unzero h0) : WithZero (Multiplicative ℤ))
Tactic: rw [← coe_unzero h0]
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
            (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯ :
              ↥(valueGroup v))) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
have neg : (↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ sorry).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
        (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
            Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) sorry :
          ↥(valueGroup v))) :
    WithZero (Multiplicative ℤ)) =
  (↑(unzero h0) : WithZero (Multiplicative ℤ))
Tactic: conv_rhs => rw [← coe_unzero h0]
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ (↑(((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm : (a : ↥(valueGroup v)) → Multiplicative ℤ)
          (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
              Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯ :
            ↥(valueGroup v))) :
      WithZero (Multiplicative ℤ)) =
    (↑(unzero h0) : WithZero (Multiplicative ℤ))
have neg : Eq (α := ↥(valueGroup v))
  (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
      Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
      (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) sorry :
    ↥(valueGroup v))
  ((intEquivOfZPowersEqTop (generator' v)⁻¹ sorry : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0) : ↥(valueGroup v))
Tactic: rw [WithZero.coe_inj, ← (MulEquiv.injective (intEquivOfZPowersEqTop _
      (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top))).eq_iff,
      MulEquiv.apply_symm_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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Eq (α := ↥(valueGroup v))
    (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
        Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
        (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯ :
      ↥(valueGroup v))
    ((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0) :
      ↥(valueGroup v))
have neg : Eq (α := WithZero (Multiplicative ℤ))
  ((↑(↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
              Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) sorry) :
          (WithZero (Multiplicative ℤ))ˣ) :
      WithZero (Multiplicative ℤ)) :
    WithZero (Multiplicative ℤ))
  ((↑(↑((intEquivOfZPowersEqTop (generator' v)⁻¹ sorry : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0)) :
          (WithZero (Multiplicative ℤ))ˣ) :
      WithZero (Multiplicative ℤ)) :
    WithZero (Multiplicative ℤ))
Tactic: ext
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑(↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑(↑((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0)) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
have neg : (v : (a : R) → WithZero (Multiplicative ℤ)) x =
  (↑(HPow.hPow (β := ℤ) (generator v) (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
    WithZero (Multiplicative ℤ))
Tactic: simp only [Units.val_mk0, intEquivOfZPowersEqTop_apply, inv_zpow', generator',
      SubgroupClass.coe_zpow]