awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : x = 0
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)

Tactic:
simp [hx0]
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
neg :
  ∀ (ϖ : R) (hϖ : Irreducible ϖ),
    Eq.{u_1 + 1} (α := Ideal R)
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
        Ideal R)
      (span {x} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
neg :
  ∀ (n : ℕ) (u : Rˣ) (hu : x = (↑u : R) * ϖ ^ n),
    Eq.{u_1 + 1} (α := Ideal R)
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
        Ideal R)
      (span {x} : Ideal R)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)

Tactic:
obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx0 hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I : Ideal R
x : R := generator I
hx0 : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hu : x = (↑u : R) * ϖ ^ n
neg :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑u : R) * ϖ ^ n)) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₁ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {(↑u : R) * ϖ ^ n} : Ideal R)
neg₂ :
  Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (↑n : ℕ∞) :
      Ideal R)
    (span {ϖ ^ n} : Ideal R)
neg₃ : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
neg₄ : HPow.hPow (α := Ideal R) (span {ϖ}) n = span {ϖ ^ n}
neg₅ neg₆ : Eq (α := Ideal R) (span {ϖ ^ n}) (span {ϖ ^ n})
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) :
      Ideal R)
    (span {x} : Ideal R)

Tactic:
rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_coe, hϖ.maximalIdeal_eq, span_singleton_pow]

Premises used: IsDiscreteValuationRing.addVal_def', ENat.recTopCoe_coe, Irreducible.maximalIdeal_eq, Ideal.span_singleton_mul_left_unit, Units.isUnit, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
n : ℕ∞ᵒᵈ
obtain :
  ∀ (k : ℕ∞),
    Eq (α := ℕ∞ᵒᵈ)
      ((fun (I : Ideal R) ↦
            ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
              ℕ∞ᵒᵈ))
          ((fun (n : ℕ∞ᵒᵈ) ↦
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                  (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
                Ideal R))
            ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k)) :
        ℕ∞ᵒᵈ)
      ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k : ℕ∞ᵒᵈ)
⊢ (fun (I : Ideal R) ↦
        ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
          ℕ∞ᵒᵈ))
      ((fun (n : ℕ∞ᵒᵈ) ↦
          (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
              ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
            Ideal R))
        n) =
    n

Tactic:
obtain ⟨k, rfl⟩ := OrderDual.toDual.surjective n

Premises used: OrderDual.toDual, Equiv.surjective, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ∞
dsimp :
  Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) k)) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k : ℕ∞ᵒᵈ)
⊢ Eq (α := ℕ∞ᵒᵈ)
    ((fun (I : Ideal R) ↦
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞) :
            ℕ∞ᵒᵈ))
        ((fun (n : ℕ∞ᵒᵈ) ↦
            (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥ (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
                ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n) :
              Ideal R))
          ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k)) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k : ℕ∞ᵒᵈ)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
⊢ Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) ⊤)) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) ⊤ : ℕ∞ᵒᵈ)

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ
coe :
  ∀ (ϖ : R) (hϖ : Irreducible ϖ),
    Eq (α := ℕ∞ᵒᵈ)
      ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
              (generator (R := R)
                (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                  (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (↑k : ℕ∞))) :
            ℕ∞) :
        ℕ∞ᵒᵈ)
      ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (↑k : ℕ∞) : ℕ∞ᵒᵈ)
⊢ Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (↑k : ℕ∞))) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (↑k : ℕ∞) : ℕ∞ᵒᵈ)

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
coe : Associated (generator (span {ϖ ^ k})) (ϖ ^ k)
⊢ Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (↑k : ℕ∞))) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (↑k : ℕ∞) : ℕ∞ᵒᵈ)

Tactic:
rw [OrderDual.toDual_inj, ENat.recTopCoe_coe, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]

Premises used: OrderDual.toDual_inj, Irreducible.addVal_pow, ENat.recTopCoe_coe, Irreducible.maximalIdeal_eq, IsDiscreteValuationRing.addVal_eq_iff_associated, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ Associated (generator (span {ϖ ^ k})) (ϖ ^ k)

Tactic:
associated_generator_span_self (ϖ ^ k)

Premises used: HPow.hPow, Submodule.IsPrincipal.associated_generator_span_self
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ Associated (generator (span {ϖ ^ k})) (ϖ ^ k)

Tactic:
exact associated_generator_span_self (ϖ ^ k)

Premises used: HPow.hPow, Submodule.IsPrincipal.associated_generator_span_self
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
k : ℕ∞
top :
  Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) ⊤)) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) ⊤ : ℕ∞ᵒᵈ)
coe :
  ∀ (k : ℕ),
    Eq (α := ℕ∞ᵒᵈ)
      ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
          (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
              (generator (R := R)
                (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                  (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) (↑k : ℕ∞))) :
            ℕ∞) :
        ℕ∞ᵒᵈ)
      ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) (↑k : ℕ∞) : ℕ∞ᵒᵈ)
⊢ Eq (α := ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
        (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞)
            (generator (R := R)
              (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n) k)) :
          ℕ∞) :
      ℕ∞ᵒᵈ)
    ((OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ) k : ℕ∞ᵒᵈ)

Tactic:
induction k with
    | top => simp
    | coe k =>
      obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
      rw [OrderDual.toDual_inj, ENat.recTopCoe_coe, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]
      exact associated_generator_span_self (ϖ ^ k)

Premises used: OrderDual.toDual_inj, IsDiscreteValuationRing.exists_irreducible, ENat.recTopCoe_coe, IsDiscreteValuationRing.addVal_eq_iff_associated, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R : Type u_1
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
I J : Ideal R
⊢ LE.le (α := ℕ∞ᵒᵈ)
      ((({
                toFun := fun (I : Ideal R) ↦
                  (OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
                    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞),
                invFun := fun (n : ℕ∞ᵒᵈ) ↦
                  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                    (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
                    ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n),
                left_inv := ⋯, right_inv := ⋯ } :
              Ideal R ≃ ℕ∞ᵒᵈ) :
            (a : Ideal R) → ℕ∞ᵒᵈ)
          I :
        ℕ∞ᵒᵈ)
      ((({
                toFun := fun (I : Ideal R) ↦
                  (OrderDual.toDual : (a : ℕ∞) → ℕ∞ᵒᵈ)
                    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (generator I) : ℕ∞),
                invFun := fun (n : ℕ∞ᵒᵈ) ↦
                  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ Ideal R) ⊥
                    (fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n)
                    ((OrderDual.ofDual : (a : ℕ∞ᵒᵈ) → ℕ∞) n),
                left_inv := ⋯, right_inv := ⋯ } :
              Ideal R ≃ ℕ∞ᵒᵈ) :
            (a : Ideal R) → ℕ∞ᵒᵈ)
          J :
        ℕ∞ᵒᵈ) ↔
    I ≤ J

Tactic:
simp [addVal_le_iff_dvd, ← span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton, IsDiscreteValuationRing.addVal_le_iff_dvd
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
⊢ (OrderIso.symm (idealOrderIsoENat R) : (a : ℕ∞ᵒᵈ) → Ideal R) (↑n : ℕ∞ᵒᵈ) = HPow.hPow (α := Ideal R) (maximalIdeal R) n

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
ϖ : R
hϖ : Irreducible ϖ
rw : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
rw₁ : HPow.hPow (α := Ideal R) (span {ϖ}) n = span {ϖ ^ n}
rw₂ rw₃ : Eq (α := Ideal R) (span {ϖ ^ n}) (span {ϖ ^ n})
⊢ Eq (α := Ideal R) ((OrderIso.symm (idealOrderIsoENat R) : (a : ℕ∞ᵒᵈ) → Ideal R) (↑n : ℕ∞ᵒᵈ) : Ideal R)
    (span {ϖ ^ n} : Ideal R)

Tactic:
rw [idealOrderIsoENat_symm_apply_coe, hϖ.maximalIdeal_eq, span_singleton_pow]

Premises used: Irreducible.maximalIdeal_eq, IsDiscreteValuationRing.idealOrderIsoENat_symm_apply_coe, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
⊢ Order.coheight (HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)

Tactic:
simpa only [Order.coheight_toDual, Order.height_enat] using
    Order.coheight_orderIso (idealOrderIsoENat R).symm (.toDual n)

Premises used: OrderDual.toDual, OrderIso.symm, Nat.cast, IsDiscreteValuationRing.idealOrderIsoENat, DFunLike.coe, Order.height_enat, Order.coheight_orderIso, Order.coheight_toDual
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
rw : Order.coheight (HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ Module.length R (R ⧸ HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)

Tactic:
rw [Module.length_quotient, coheight_pow_maximalIdeal]

Premises used: Module.length_quotient, IsDiscreteValuationRing.coheight_pow_maximalIdeal
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x : R
hx : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (HPow.hPow (α := Ideal R) (maximalIdeal R) n) ⊤) x 0
obtain : ∀ (ϖ : R) (hϖ : Irreducible ϖ), x = 0
⊢ x = 0

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x : R
hx : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (HPow.hPow (α := Ideal R) (maximalIdeal R) n) ⊤) x 0
ϖ : R
hϖ : Irreducible ϖ
⊢ ∀ (n : ℕ), LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)

Tactic:
simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.zero, hϖ.maximalIdeal_eq,
      Ideal.span_singleton_pow, Ideal.mem_span_singleton, ← addVal_le_iff_dvd, hϖ.addVal_pow] at hx

Premises used: Ideal.one_eq_top, SModEq.zero, Irreducible.addVal_pow, Irreducible.maximalIdeal_eq, smul_eq_mul, mul_one, IsDiscreteValuationRing.addVal_le_iff_dvd, Ideal.mem_span_singleton, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R_1 : Type u
inst : CommRing R_1
inst_1 : IsDomain R_1
inst_2 : IsDiscreteValuationRing R_1
R_2 : Type u_1
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : IsDiscreteValuationRing R
x ϖ : R
hϖ : Irreducible ϖ
hx : ∀ (n : ℕ), LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
rwa : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (b : ℕ), (↑b : WithTop ℕ) ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
⊢ x = 0

Tactic:
rwa [← addVal_eq_top_iff, WithTop.eq_top_iff_forall_ge]

Premises used: WithTop.eq_top_iff_forall_ge, IsDiscreteValuationRing.addVal_eq_top_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ toWithBotNat.{u_2} (R := R) 0 = ⊥

Tactic:
addVal_zero

Premises used: IsDiscreteValuationRing.addVal_zero, WithBot, IsDiscreteValuationRing.toWithBotNat, ENat
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
⊢ toWithBotNat x = ⊥ ↔ x = 0

Tactic:
addVal_eq_top_iff

Premises used: WithBot, IsDiscreteValuationRing.toWithBotNat, ENat, IsDiscreteValuationRing.addVal_eq_top_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
rw : toWithBotNat x ≠ ⊥ ↔ x ≠ 0
⊢ ⊥ < toWithBotNat x ↔ x ≠ 0

Tactic:
rw [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
⊢ toWithBotNat x ≠ ⊥ ↔ x ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
generalize :
  ∀ (vx : ℕ∞) (hvx : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x = vx),
    vx ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y ↔ x ∣ y
⊢ LE.le (α := WithBot ℕ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ↔
    x ∣ y

Tactic:
generalize hvx : addVal R x = vx

Premises used: IsDiscreteValuationRing.addVal, DFunLike.coe
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ∞
hvx : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x = vx
generalize : ∀ (vy : ℕ∞) (hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy), vx ≤ vy ↔ x ∣ y
⊢ vx ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y ↔ x ∣ y

Tactic:
generalize hvy : addVal R y = vy

Premises used: IsDiscreteValuationRing.addVal, DFunLike.coe
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)
⊢ x = 0

Tactic:
rw [addVal_eq_top_iff] at hvx

Premises used: IsDiscreteValuationRing.addVal_eq_top_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
hvx : x = 0
⊢ ⊤ ≤ vy ↔ x ∣ y

Tactic:
tauto
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) (⊤ : ℕ∞)
⊢ y = 0

Tactic:
rw [addVal_eq_top_iff] at hvy

Premises used: IsDiscreteValuationRing.addVal_eq_top_iff
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
hvy : y = 0
⊢ LE.le (α := WithBot ℕ) (↑vx : ℕ∞) ⊤ ↔ x ∣ y

Tactic:
tauto
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
vy : ℕ
hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ((↑vy : ℕ∞) : ℕ∞)
coe : LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ LE.le (α := ℕ∞) (↑vx : ℕ∞) (↑vy : ℕ∞)
⊢ LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ x ∣ y

Tactic:
rw [← addVal_le_iff_dvd, hvx, hvy]

Premises used: IsDiscreteValuationRing.addVal_le_iff_dvd
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
vy : ℕ
hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ((↑vy : ℕ∞) : ℕ∞)
⊢ LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ LE.le (α := ℕ∞) (↑vx : ℕ∞) (↑vy : ℕ∞)

Tactic:
WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

Premises used: WithBot.some, WithBot.coe_le_coe, WithTop.some, Iff.trans, WithTop.coe_le_coe, Iff.symm
-- Module: Mathlib.RingTheory.DiscreteValuationRing.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
vy : ℕ
hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ((↑vy : ℕ∞) : ℕ∞)
⊢ LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ LE.le (α := ℕ∞) (↑vx : ℕ∞) (↑vy : ℕ∞)

Tactic:
exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm

Premises used: WithBot.coe_le_coe, Iff.trans, WithTop.coe_le_coe, Iff.symm