awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ (b : ↥v.valuationSubring), a * b = 1
⊢ (↑π : K) ≠ 0

Tactic:
have := hπ.ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ (b : ↥v.valuationSubring), a * b = 1
this : (↑π : K) ≠ 0
⊢ ¬π = 0

Tactic:
simp only [ne_eq, Subring.coe_eq_zero_iff] at this

Premises used: ne_eq, Subring.coe_eq_zero_iff
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ (b : ↥v.valuationSubring), a * b = 1
this : ¬π = 0
⊢ ∃ (b : ↥v.valuationSubring), π * b = 1

Tactic:
specialize h this
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
this : ¬π = 0
h : ∃ (b : ↥v.valuationSubring), π * b = 1
⊢ IsUnit π

Tactic:
rw [← isUnit_iff_exists_inv] at h

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
this : ¬π = 0
h : IsUnit π
⊢ False

Tactic:
hπ.not_isUnit h

Premises used: Valuation.IsUniformizer.not_isUnit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : Nontrivial.{u_1} ↥(valueGroup v)
inst_3 : IsCyclic.{u_1} ↥(valueGroup v)
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
this : ¬π = 0
h : IsUnit π
⊢ False

Tactic:
exact hπ.not_isUnit h

Premises used: Valuation.IsUniformizer.not_isUnit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
h : r = 0
⊢ Eq.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥

Tactic:
rw [h, Set.singleton_zero, span_zero] at hr

Premises used: Ideal.span_zero, Set.singleton_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
h : r = 0
hr₁ : Eq.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥
⊢ r = 0

Tactic:
rw [h, Set.singleton_zero, span_zero] at hr

Premises used: Ideal.span_zero, Set.singleton_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥
h : r = 0
⊢ False

Tactic:
Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr

Premises used: Ring.ne_bot_of_isMaximal_of_not_isField, Membership.mem, Subtype, IsLocalRing.maximalIdeal.isMaximal, Valuation.valuationSubring_not_isField, Valuation.valuationSubring
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥
h : r = 0
⊢ False

Tactic:
exact Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr

Premises used: Ring.ne_bot_of_isMaximal_of_not_isField, Membership.mem, Subtype, IsLocalRing.maximalIdeal.isMaximal, Valuation.valuationSubring_not_isField, Valuation.valuationSubring
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
⊢ r ≠ 0

Tactic:
have hr₀ : r ≠ 0 := by
    intro h
    rw [h, Set.singleton_zero, span_zero] at hr
    exact Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal v.valuationSubring)
      (valuationSubring_not_isField v) hr
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
hr₀ : r ≠ 0
obtain : ∀ (π : ↥v.valuationSubring) (hπ : v.IsUniformizer (↑π : K)), v.IsUniformizer (↑r : K)
⊢ v.IsUniformizer (↑r : K)

Tactic:
obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v

Premises used: Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
obtain :
  ∀ (n : ℕ) (u : (↥v.valuationSubring)ˣ)
    (hu :
      (↑r : K) =
        (↑({ val := π, valuation_gt_one := hπ : v.Uniformizer }.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
    v.IsUniformizer (↑r : K)
⊢ v.IsUniformizer (↑r : K)

Tactic:
obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩

Premises used: Valuation.Uniformizer.mk, Valuation.exists_pow_Uniformizer
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {r})
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
n : ℕ
u : (↥v.valuationSubring)ˣ
hu :
  (↑r : K) = (↑({ val := π, valuation_gt_one := hπ : v.Uniformizer }.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
rw :
  ∀ (hr : Associated { val := π, valuation_gt_one := hπ : v.Uniformizer }.val r) (n : ℕ) (u : (↥v.valuationSubring)ˣ)
    (hu :
      (↑r : K) =
        (↑({ val := π, valuation_gt_one := hπ : v.Uniformizer }.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
    v.IsUniformizer (↑r : K)
⊢ v.IsUniformizer (↑r : K)

Tactic:
rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr

Premises used: Ideal.span_singleton_eq_span_singleton, Valuation.Uniformizer.mk, Valuation.Uniformizer.is_generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
hr : Associated { val := π, valuation_gt_one := hπ : v.Uniformizer }.val r
n : ℕ
u : (↥v.valuationSubring)ˣ
hu :
  (↑r : K) = (↑({ val := π, valuation_gt_one := hπ : v.Uniformizer }.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ v.IsUniformizer (↑r : K)

Tactic:
hπ.of_associated hr

Premises used: Valuation.IsUniformizer.of_associated
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer (↑π : K)
hr : Associated { val := π, valuation_gt_one := hπ : v.Uniformizer }.val r
n : ℕ
u : (↥v.valuationSubring)ˣ
hu :
  (↑r : K) = (↑({ val := π, valuation_gt_one := hπ : v.Uniformizer }.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ v.IsUniformizer (↑r : K)

Tactic:
exact hπ.of_associated hr

Premises used: Valuation.IsUniformizer.of_associated
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I : Ideal ↥v.valuationSubring
this : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal I

Tactic:
(IsPrincipalIdealRing.of_prime this).principal I

Premises used: IsPrincipalIdealRing.principal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I : Ideal ↥v.valuationSubring
this : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal I

Tactic:
exact (IsPrincipalIdealRing.of_prime this).principal I

Premises used: IsPrincipalIdealRing.principal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I : Ideal ↥v.valuationSubring
suffices : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal I

Tactic:
suffices ∀ P : Ideal K₀, P.IsPrime → Submodule.IsPrincipal P by
    exact (IsPrincipalIdealRing.of_prime this).principal I
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
pos : ∀ (h_ne_bot : P = ⊥), Submodule.IsPrincipal P
neg : ∀ (h_ne_bot : ¬P = ⊥), Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P

Tactic:
by_cases h_ne_bot : P = ⊥
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : P = ⊥
pos : Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (M := ↥v.valuationSubring) ⊥
⊢ Submodule.IsPrincipal P

Tactic:
rw [h_ne_bot]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : P = ⊥
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (M := ↥v.valuationSubring) ⊥

Tactic:
bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : P = ⊥
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (M := ↥v.valuationSubring) ⊥

Tactic:
exact bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
⊢ Nonempty.{u_2 + 1} v.Uniformizer

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
neg : ∀ (x : ↥v.valuationSubring) (hx_mem : x ∈ P) (hx₀ : x ≠ 0), Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨x, ⟨hx_mem, hx₀⟩⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
neg :
  ∀ (n : ℕ) (u : (↥v.valuationSubring)ˣ) (hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
    Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π

Premises used: Valuation.exists_pow_Uniformizer
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
pos : ∀ (hn : n = 0), Submodule.IsPrincipal P
neg : ∀ (hn : ¬n = 0), Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
hn : n = 0
⊢ x = (↑u : ↥v.valuationSubring)

Tactic:
rw [← Subring.coe_mul, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu

Premises used: SetLike.coe_eq_coe, Subring.coe_mul, pow_zero, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
hn : n = 0
hu₁ : x = (↑u : ↥v.valuationSubring)
⊢ n = 0

Tactic:
rw [← Subring.coe_mul, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu

Premises used: SetLike.coe_eq_coe, Subring.coe_mul, pow_zero, one_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = (↑u : ↥v.valuationSubring)
hn : n = 0
⊢ Submodule.IsPrincipal P

Tactic:
(hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim

Premises used: False.elim, Ideal.eq_top_of_isUnit_mem, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = (↑u : ↥v.valuationSubring)
hn : n = 0
pos : IsUnit x
⊢ Submodule.IsPrincipal P

Tactic:
refine (hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim

Premises used: False.elim, Ideal.eq_top_of_isUnit_mem, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = (↑u : ↥v.valuationSubring)
hn : n = 0
⊢ IsUnit x

Tactic:
simp only [hu, Units.isUnit]

Premises used: Units.isUnit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
hn : ¬n = 0
⊢ x = π.val ^ n * (↑u : ↥v.valuationSubring)

Tactic:
rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu

Premises used: SetLike.coe_eq_coe, Subring.coe_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
hn : ¬n = 0
hu₁ : x = π.val ^ n * (↑u : ↥v.valuationSubring)
⊢ ¬n = 0

Tactic:
rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu

Premises used: SetLike.coe_eq_coe, Subring.coe_mul
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
⊢ span {π.val} ≤ P

Tactic:
rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem

Premises used: Iff.mpr, Ideal.IsPrime.pow_mem_iff_mem, Ideal.span_singleton_le_iff_mem, Ideal.mul_unit_mem_iff_mem, Units.isUnit, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
hx_mem₁ : span {π.val} ≤ P
⊢ x = π.val ^ n * (↑u : ↥v.valuationSubring)

Tactic:
rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem

Premises used: Iff.mpr, Ideal.IsPrime.pow_mem_iff_mem, Ideal.span_singleton_le_iff_mem, Ideal.mul_unit_mem_iff_mem, Units.isUnit, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
hx_mem₁ : span {π.val} ≤ P
hu₁ : x = π.val ^ n * (↑u : ↥v.valuationSubring)
⊢ ¬n = 0

Tactic:
rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at hx_mem

Premises used: Iff.mpr, Ideal.IsPrime.pow_mem_iff_mem, Ideal.span_singleton_le_iff_mem, Ideal.mul_unit_mem_iff_mem, Units.isUnit, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hx_mem : span {π.val} ≤ P
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
⊢ maximalIdeal ↥v.valuationSubring ≤ P

Tactic:
replace hx_mem := π.is_generator ▸ hx_mem
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
hx_mem : maximalIdeal ↥v.valuationSubring ≤ P
neg : Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring)
⊢ Submodule.IsPrincipal P

Tactic:
rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := Nonempty.some ⋯
x : ↥v.valuationSubring
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
hx_mem : maximalIdeal ↥v.valuationSubring ≤ P
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring)

Tactic:
⟨π.1, π.is_generator⟩

Premises used: Valuation.Uniformizer.val, Submodule.IsPrincipal.mk, Exists.intro, Valuation.Uniformizer.is_generator