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 : 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:
exact ⟨π.1, π.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 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ IsPrincipalIdealRing.{u_2} ↥v.valuationSubring

Tactic:
⟨fun I ↦ ideal_isPrincipal v I⟩

Premises used: Valuation.ideal_isPrincipal, IsPrincipalIdealRing.mk
-- 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)
rw : ¬IsField.{u_2} ↥v.valuationSubring
⊢ Ne.{u_2 + 1} (α := Ideal ↥v.valuationSubring) (maximalIdeal ↥v.valuationSubring) ⊥

Tactic:
rw [ne_eq, ← isField_iff_maximalIdeal_eq]

Premises used: IsLocalRing.isField_iff_maximalIdeal_eq, ne_eq
-- 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)
⊢ ¬IsField.{u_2} ↥v.valuationSubring

Tactic:
valuationSubring_not_isField v

Premises used: Valuation.valuationSubring_not_isField
-- 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)
⊢ ¬IsField.{u_2} ↥v.valuationSubring

Tactic:
exact valuationSubring_not_isField v

Premises used: Valuation.valuationSubring_not_isField
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
⊢ Ne (α := Ideal A) (IsLocalRing.maximalIdeal A) ⊥

Tactic:
simpa [ne_eq, ← isField_iff_maximalIdeal_eq] using not_isField A

Premises used: IsDiscreteValuationRing.not_isField, IsLocalRing.isField_iff_maximalIdeal_eq, ne_eq
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ)))
    ⋯
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))
rw :
  ∃ (x : (WithZero (Multiplicative ℤ))ˣ),
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
        (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) x ∧
      x ≠ 1
⊢ Nontrivial ↥(valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))

Tactic:
rw [Subgroup.nontrivial_iff_exists_ne_one]

Premises used: Subgroup.nontrivial_iff_exists_ne_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ)) ((v : (a : K) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [hπ]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))ˣ) ∧
    Ne (α := (WithZero (Multiplicative ℤ))ˣ)
      (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
      (1 : (WithZero (Multiplicative ℤ))ˣ)
⊢ ∃ (x : (WithZero (Multiplicative ℤ))ˣ),
    Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ)
        (valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) x ∧
      x ≠ 1

Tactic:
use Units.mk0 (v π) (by simp [hπ])

Premises used: Units.mk0, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))ˣ)
h₁ :
  Ne (α := (WithZero (Multiplicative ℤ))ˣ)
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
    (1 : (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 ℤ))ˣ)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ)) (γ := Set (WithZero (Multiplicative ℤ)))
    (Set.range (ι := K) (⇑(valuation K (maximalIdeal A)) : (a : K) → WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯) : 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 ℤ))ˣ)

Tactic:
apply mem_valueGroup

Premises used: MonoidWithZeroHom.mem_valueGroup
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
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 ℤ))
⊢ ∃ (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 ℤ))

Tactic:
use π
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))
⊢ Ne (α := (WithZero (Multiplicative ℤ))ˣ)
    (Units.mk0 ((v : (a : K) → WithZero (Multiplicative ℤ)) π) ⋯ : (WithZero (Multiplicative ℤ))ˣ)
    (1 : (WithZero (Multiplicative ℤ))ˣ)

Tactic:
simpa [hπ] using not_eq_of_beq_eq_false rfl

Premises used: not_eq_of_beq_eq_false
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
this : Nontrivial ↥(valueGroup (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
⊢ IsRankOneDiscrete (valuation K (maximalIdeal A))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 ℤ))
obtain : ∀ (π : A) (hπ : Irreducible π), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
obtain ⟨π, hπ⟩ := exists_irreducible A

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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 π
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
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
obtain ⟨a, b, hb, h_frac⟩ := IsFractionRing.div_surjective A x

Premises used: IsFractionRing.div_surjective
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
neg : ∀ (ha : ¬a = 0), ∃ (a : A), (algebraMap A K : (a : A) → K) a = x
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
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)
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = x

Tactic:
rw [← h_frac]
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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) a : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ ∃ (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:
use 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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)
h₂ h₃ : Eq.{u_2 + 1} (α := K) 0 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)

Tactic:
rw [ha, map_zero, zero_div]

Premises used: zero_div, map_zero
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [← h_frac] at H
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
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₁ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b

Tactic:
rw [← h_frac] at H