awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = π.val ^ n * (↑u : ↥v.valuationSubring)
Tactic: rw [← Subring.coe_mul, SetLike.coe_eq_coe] at hu
Cleared hypotheses: hu, hn
-- 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 = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
⊢ Submodule.IsPrincipal P
have hx_mem₁ : 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
Cleared hypotheses: hx_mem, hu, hn
-- 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₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hx_mem : span {π.val} ≤ P
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
⊢ Submodule.IsPrincipal P
have hx_mem₁ : maximalIdeal ↥v.valuationSubring ≤ P
Tactic: replace hx_mem := π.is_generator ▸ hx_mem
Cleared hypotheses: hx_mem
-- 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₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * (↑u : ↥v.valuationSubring)
hn : ¬n = 0
hx_mem : maximalIdeal ↥v.valuationSubring ≤ P
⊢ Submodule.IsPrincipal P
have neg : Submodule.IsPrincipal.{u_2, u_2} (R := ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring)
Tactic: rw [← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem]
-- 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)
⊢ Ne.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥
have rw : ¬IsField.{u_2} ↥v.valuationSubring
Tactic: rw [ne_eq, ← isField_iff_maximalIdeal_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
⊢ Nontrivial ↥(valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
have hπ : Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
  ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
Tactic: have hπ : v π = ↑(ofAdd (-1 : ℤ)) :=
      valuation_exists_uniformizer K (maximalIdeal A) |>.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ Nontrivial ↥(valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
have rw : ∃ (x : (WithZero (Multiplicative ℤ))ˣ),
  Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
      (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) x ∧
    x ≠ 1
Tactic: rw [Subgroup.nontrivial_iff_exists_ne_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ ∃ (x : (WithZero (Multiplicative ℤ))ˣ),
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
        (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) x ∧
      x ≠ 1
have h : Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
    (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) sorry : (WithZero (Multiplicative ℤ))ˣ) ∧
  Ne (α := (WithZero (Multiplicative ℤ))ˣ)
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) sorry : (WithZero (Multiplicative ℤ))ˣ)
    (1 : (WithZero (Multiplicative ℤ))ˣ)
Tactic: use Units.mk0 (v π) (by simp [hπ])
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
      (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
      (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ) ∧
    Ne (α := (WithZero (Multiplicative ℤ))ˣ)
      (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
      (1 : (WithZero (Multiplicative ℤ))ˣ)
have h : Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
  (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
  (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) sorry : (WithZero (Multiplicative ℤ))ˣ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
h :
  Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
    (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
⊢ Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
      (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
      (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ) ∧
    Ne (α := (WithZero (Multiplicative ℤ))ˣ)
      (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
      (1 : (WithZero (Multiplicative ℤ))ˣ)
have h₁ : Ne (α := (WithZero (Multiplicative ℤ))ˣ)
  (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) sorry : (WithZero (Multiplicative ℤ))ˣ)
  (1 : (WithZero (Multiplicative ℤ))ˣ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
⊢ Membership.mem (α := (WithZero (Multiplicative ℤ))ˣ) (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
    (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
have h : Membership.mem (α := WithZero (Multiplicative ℤ)) (γ := Set (WithZero (Multiplicative ℤ)))
  (Set.range (ι := K) (⇑(valuation K (maximalIdeal A)) : (a : K) → WithZero (Multiplicative ℤ)))
  ((↑(Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) sorry) : WithZero (Multiplicative ℤ)) :
    WithZero (Multiplicative ℤ))
Tactic: apply mem_valueGroup
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
v : Valuation K (WithZero (Multiplicative ℤ)) := valuation K (maximalIdeal A)
π : K :=
  Exists.choose (p := fun (π : K) ↦
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          π :
        WithZero (Multiplicative ℤ))
      (WithZero.exp (-1) : WithZero (Multiplicative ℤ)))
    ⋯
hπ :
  Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    ((↑((ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) : WithZero (Multiplicative ℤ))
w : K
⊢ ∃ (y : K),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          y :
        WithZero (Multiplicative ℤ))
      ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      π :
    WithZero (Multiplicative ℤ))
  ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
Tactic: use π
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ IsRankOneDiscrete (valuation K (maximalIdeal A))
have this : Nontrivial ↥(valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
Tactic: have : Nontrivial ↥(valueGroup (valuation K (maximalIdeal A))) := by
    let v := (maximalIdeal A).valuation K
    let π := valuation_exists_uniformizer K (maximalIdeal A) |>.choose
    have hπ : v π = ↑(ofAdd (-1 : ℤ)) :=
      valuation_exists_uniformizer K (maximalIdeal A) |>.choose_spec
    rw [Subgroup.nontrivial_iff_exists_ne_one]
    use Units.mk0 (v π) (by simp [hπ])
    constructor
    · apply mem_valueGroup
      simp only [Units.val_mk0, Set.mem_range]
      use π
    · simpa [hπ] using not_eq_of_beq_eq_false rfl
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have obtain : ∀ (π : A) (hπ : Irreducible π), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
Tactic: obtain ⟨π, hπ⟩ := exists_irreducible A
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have obtain : ∀ (a b : A) (hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b)
  (h_frac :
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x),
  ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
Tactic: obtain ⟨a, b, hb, h_frac⟩ := IsFractionRing.div_surjective A x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have pos : ∀ (ha : a = 0), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
pos : ∀ (ha : a = 0), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have neg : ∀ (ha : ¬a = 0), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : a = 0
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
have pos : ∃ (a_1 : A),
  (algebraMap A K : (a : A) → K) a_1 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: rw [← h_frac]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : a = 0
⊢ ∃ (a_1 : A),
    (algebraMap A K : (a : A) → K) a_1 =
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
have h : (algebraMap A K : (a : A) → K) 0 =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : a = 0
⊢ (algebraMap A K : (a : A) → K) 0 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
have h : (algebraMap A K : (a : A) → K) 0 =
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) 0 : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: rw [ha, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : a = 0
h :
  (algebraMap A K : (a : A) → K) 0 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) 0 : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ (algebraMap A K : (a : A) → K) 0 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
have h₁ : 0 = HDiv.hDiv (α := K) (β := K) (0 : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: rw [ha, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
π : A
hπ : Irreducible π
a b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b
h_frac : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) = x
ha : a = 0
h :
  (algebraMap A K : (a : A) → K) 0 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) 0 : K) ((algebraMap A K : (a : A) → K) b : K)
h₁ : 0 = HDiv.hDiv (α := K) (β := K) (0 : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ (algebraMap A K : (a : A) → K) 0 =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
have h₂ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [ha, map_zero, zero_div]