awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (π : 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
⊢ ∃ (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

Tactic:
have ⟨π, hπ⟩ := hπ
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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

Tactic:
⟨1, ?_, π ^ n, ?_⟩

Premises used: HPow.hPow, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
hH₁ :
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
      (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n)) :
        WithZero (Multiplicative ℤ)) =
    (v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ 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)) :
              WithZero (Multiplicative ℤ)) =
          (v : (a : R) → WithZero (Multiplicative ℤ)) x

Tactic:
refine ⟨1, ?_, π ^ n, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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
⊢ ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [hπ]
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) 1 : WithZero (Multiplicative ℤ))
      (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.ofNat n)) :
        WithZero (Multiplicative ℤ)) =
    (v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ n)

Tactic:
simp [hπ]
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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

Tactic:
⟨π ^ (n + 1), ?_, 1, ?_⟩

Premises used: HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
hH₁ :
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
      (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.negSucc n)) :
        WithZero (Multiplicative ℤ)) =
    (v : (a : R) → WithZero (Multiplicative ℤ)) 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

Tactic:
refine ⟨π ^ (n + 1), ?_, 1, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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
⊢ ¬Eq (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [hπ, Int.negSucc_eq, mul_assoc]

Premises used: mul_assoc, Int.negSucc_eq
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ))
      ((v : (a : R) → WithZero (Multiplicative ℤ)) (π ^ (n + 1)) : WithZero (Multiplicative ℤ))
      (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (Int.negSucc n)) :
        WithZero (Multiplicative ℤ)) =
    (v : (a : R) → WithZero (Multiplicative ℤ)) 1

Tactic:
simp [hπ, Int.negSucc_eq, mul_assoc]

Premises used: mul_assoc, Int.negSucc_eq
-- 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π_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
hH₁ :
  ∀ (n_1 : ℕ) (h : HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (Units.mk0 (exp 1)⁻¹ ⋯) (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)⁻¹ ⋯) (Int.negSucc 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

Tactic:
cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]

Premises used: mul_assoc, Int.negSucc_eq
-- 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
⊢ 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
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := R) (⇑v : (a : R) → WithZero (Multiplicative ℤ))) (exp (-1))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
generator_eq_exp_neg_one_of_surjective hsurj

Premises used: Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
neg :
  ∀
    (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 ℤ))
          ((↑(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 ↥(valueGroup v)) :
            WithZero ↥(valueGroup v)) :
        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 ℤ))

Tactic:
split_ifs with h0
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
    ((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 ℤ))

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
rw : (↑(unzero h0) : WithZero (Multiplicative ℤ))
| (v : (a : R) → WithZero (Multiplicative ℤ)) x

Tactic:
rw [← coe_unzero h0]

Premises used: WithZero.coe_unzero
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
neg :
  (↑(((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 ℤ))
⊢ 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 ℤ))

Tactic:
conv_rhs => rw [← coe_unzero h0]

Premises used: WithZero.coe_unzero
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
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 ℤ))
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) ⋯ :
      ↥(valueGroup v))
    ((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0) :
      ↥(valueGroup v))
⊢ (↑(((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 ℤ))

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]

Premises used: WithZero.coe_inj, Function.Injective.eq_iff, intEquivOfZPowersEqTop, MulEquiv.injective, MulEquiv.apply_symm_apply