awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
h_unit_a : IsUnit a
h : (↑r : K) = (↑(π.val ^ n) : K) * (↑a : K)
h₁ : (↑r : K) = (↑π.val : K) ^ n * (↑a : K)
h₂ :
  (↑r : K) =
    (↑π.val : K) ^ n *
      (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯) : K)
h₃ : (↑r : K) = (↑π.val : K) ^ n * (↑π.val : K) ^ (-m) * (↑r : K)
h₄ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ m)⁻¹ * (↑r : K)
h₅ : (↑r : K) = (↑π.val : K) ^ n * (HPow.hPow (β := ℤ) (↑π.val : K) (↑n : ℤ))⁻¹ * (↑r : K)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₆ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ n)⁻¹ * (↑r : K)
Tactic: rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
h_unit_a : IsUnit a
h : (↑r : K) = (↑(π.val ^ n) : K) * (↑a : K)
h₁ : (↑r : K) = (↑π.val : K) ^ n * (↑a : K)
h₂ :
  (↑r : K) =
    (↑π.val : K) ^ n *
      (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯) : K)
h₃ : (↑r : K) = (↑π.val : K) ^ n * (↑π.val : K) ^ (-m) * (↑r : K)
h₄ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ m)⁻¹ * (↑r : K)
h₅ : (↑r : K) = (↑π.val : K) ^ n * (HPow.hPow (β := ℤ) (↑π.val : K) (↑n : ℤ))⁻¹ * (↑r : K)
h₆ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ n)⁻¹ * (↑r : K)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₇ : (↑r : K) = 1 * (↑r : K)
Tactic: rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : Ne.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑r : K) : Γ) (0 : Γ)
vr : Γˣ := Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
hvr_def : vr = Units.mk0 ((v : (a : K) → Γ) (↑r : K)) hr₀
m : ℤ
hm : HPow.hPow (α := Γˣ) (Units.mk0 ((v : (a : K) → Γ) (↑π.val : K)) ⋯ : Γˣ) m = vr
hm' : HPow.hPow (α := Γ) ((v : (a : K) → Γ) (↑π.val : K) : Γ) m = (v : (a : K) → Γ) (↑r : K)
hm₀ : 0 ≤ m
n : ℕ
hn : m = (↑n : ℤ)
hpow : Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) ((↑π.val : K) ^ (-m) * (↑r : K)) : Γ) (1 : Γ)
a : ↥v.valuationSubring := Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha : a = Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯
ha₀ : (↑a : K) ≠ 0
h_unit_a : IsUnit a
h : (↑r : K) = (↑(π.val ^ n) : K) * (↑a : K)
h₁ : (↑r : K) = (↑π.val : K) ^ n * (↑a : K)
h₂ :
  (↑r : K) =
    (↑π.val : K) ^ n *
      (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ v.valuationSubring) ((↑π.val : K) ^ (-m) * (↑r : K)) ⋯) : K)
h₃ : (↑r : K) = (↑π.val : K) ^ n * (↑π.val : K) ^ (-m) * (↑r : K)
h₄ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ m)⁻¹ * (↑r : K)
h₅ : (↑r : K) = (↑π.val : K) ^ n * (HPow.hPow (β := ℤ) (↑π.val : K) (↑n : ℤ))⁻¹ * (↑r : K)
h₆ : (↑r : K) = (↑π.val : K) ^ n * ((↑π.val : K) ^ n)⁻¹ * (↑r : K)
h₇ : (↑r : K) = 1 * (↑r : K)
⊢ (↑r : K) = (↑(π.val ^ n) : K) * (↑(↑h_unit_a.unit : ↥v.valuationSubring) : K)
have h₈ : (↑r : K) = (↑r : K)
Tactic: rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
⊢ Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π.val})
have hJ : Ne (α := Ideal ↥v.valuationSubring) (span {π.val}) ⊤
Tactic: apply (maximalIdeal.isMaximal _).eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
hJ : Ne (α := Ideal ↥v.valuationSubring) (span {π.val}) ⊤
⊢ Eq (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π.val})
have IJ : LE.le (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) (span {π.val})
Tactic: apply (maximalIdeal.isMaximal _).eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
h : Eq (α := Ideal ↥v.valuationSubring) (span {π.val}) ⊤
⊢ False
have h₁ : IsUnit π.val
Tactic: rw [Ideal.span_singleton_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have pos : ∀ (hx₀ : x = 0), Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
Tactic: by_cases hx₀ : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
pos : ∀ (hx₀ : x = 0), Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have neg : ∀ (hx₀ : ¬x = 0), Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
Tactic: by_cases hx₀ : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have neg : ∀ (n : ℕ) (u : (↥v.valuationSubring)ˣ) (hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
  Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
Tactic: obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have hu₁ : x = π.val ^ n * (↑u : ↥v.valuationSubring)
Tactic: rw [← Subring.coe_mul, Subtype.coe_inj] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have hn : ¬IsUnit x
Tactic: have hn : Not (IsUnit x) := fun h ↦
        (maximalIdeal.isMaximal _).ne_top (eq_top_of_isUnit_mem _ hx h)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) x
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬IsUnit x
⊢ Membership.mem (γ := Submodule ↥v.valuationSubring ↥v.valuationSubring) (span {π.val}) x
have hn₁ : n ≠ 0
Tactic: replace hn : n ≠ 0 := fun h ↦ by
        simp only [hu, h, pow_zero, one_mul, Units.isUnit, not_true] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
n : ℕ
⊢ HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n = span {π.val ^ n}
have rw : HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n =
  HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
Tactic: rw [← Ideal.span_singleton_pow, Uniformizer.is_generator]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
n : ℕ
rw :
  HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n =
    HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
⊢ HPow.hPow (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) n = span {π.val ^ n}
have rw₁ : HPow.hPow (α := Ideal ↥v.valuationSubring) (span {π.val}) n = HPow.hPow (α := Ideal ↥v.integer) (span {π.val}) n
Tactic: rw [← Ideal.span_singleton_pow, Uniformizer.is_generator]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ ¬IsField.{u_2} ↥v.valuationSubring
have obtain : ∀ (π : ↥v.valuationSubring) (hπ : v.IsUniformizer (↑π : K)), ¬IsField.{u_2} ↥v.valuationSubring
Tactic: obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ False
have this : (↑π : K) ≠ 0
Tactic: have := hπ.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ False
have this₁ : ¬π = 0
Tactic: simp only [ne_eq, Subring.coe_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ False
have h₁ : ∃ (b : ↥v.valuationSubring), π * b = 1
Tactic: specialize h this
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ False
have h₁ : IsUnit π
Tactic: rw [← isUnit_iff_exists_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ False
have hr₁ : Eq.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥
Tactic: rw [h, Set.singleton_zero, span_zero] at hr
Cleared hypotheses: hr, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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})
⊢ v.IsUniformizer (↑r : K)
have hr₀ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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.IsUniformizer (↑r : K)
have obtain : ∀ (π : ↥v.valuationSubring) (hπ : v.IsUniformizer (↑π : K)), v.IsUniformizer (↑r : K)
Tactic: obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ v.IsUniformizer (↑r : K)
have 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)
Tactic: obtain ⟨n, u, hu⟩ := exists_pow_Uniformizer hr₀ ⟨π, hπ⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ v.IsUniformizer (↑r : K)
have 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)
Tactic: rw [Uniformizer.is_generator ⟨π, hπ⟩, span_singleton_eq_span_singleton] at hr
Cleared hypotheses: hr, n, u, hu
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Submodule.IsPrincipal I
have suffices : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
Tactic: suffices ∀ P : Ideal K₀, P.IsPrime → Submodule.IsPrincipal P by
    exact (IsPrincipalIdealRing.of_prime this).principal I
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Submodule.IsPrincipal P
have pos : ∀ (h_ne_bot : P = ⊥), Submodule.IsPrincipal P
Tactic: by_cases h_ne_bot : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Submodule.IsPrincipal P
have neg : ∀ (h_ne_bot : ¬P = ⊥), Submodule.IsPrincipal P
Tactic: by_cases h_ne_bot : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 P
have pos : Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (M := ↥v.valuationSubring) ⊥
Tactic: rw [h_ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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 ⋯
⊢ Submodule.IsPrincipal P
have neg : ∀ (x : ↥v.valuationSubring) (hx_mem : x ∈ P) (hx₀ : x ≠ 0), Submodule.IsPrincipal P
Tactic: obtain ⟨x, ⟨hx_mem, hx₀⟩⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h_ne_bot
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Submodule.IsPrincipal P
have neg : ∀ (n : ℕ) (u : (↥v.valuationSubring)ˣ) (hu : (↑x : K) = (↑(π.val ^ n) : K) * (↑(↑u : ↥v.valuationSubring) : K)),
  Submodule.IsPrincipal P
Tactic: obtain ⟨n, ⟨u, hu⟩⟩ := exists_pow_Uniformizer hx₀ π
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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)
⊢ Submodule.IsPrincipal P
have pos : ∀ (hn : n = 0), Submodule.IsPrincipal P
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
⊢ Submodule.IsPrincipal P
have neg : ∀ (hn : ¬n = 0), Submodule.IsPrincipal P
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
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
⊢ Submodule.IsPrincipal P
have hu₁ : x = (↑u : ↥v.valuationSubring)
Tactic: rw [← Subring.coe_mul, hn, pow_zero, one_mul, SetLike.coe_eq_coe] at hu
Cleared hypotheses: hu, hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
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
have pos : IsUnit x
Tactic: refine (hP.ne_top (Ideal.eq_top_of_isUnit_mem P hx_mem ?_)).elim