awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞ᵒᵈ
⊢ (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
have 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 : ℕ∞ᵒᵈ)
Tactic: obtain ⟨k, rfl⟩ := OrderDual.toDual.surjective n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞
⊢ 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 : ℕ∞ᵒᵈ)
have 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 : ℕ∞ᵒᵈ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ
⊢ 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 : ℕ∞) : ℕ∞ᵒᵈ)
have 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 : ℕ∞) : ℕ∞ᵒᵈ)
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 ϖ
⊢ 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 : ℕ∞) : ℕ∞ᵒᵈ)
have coe : Associated (generator (span {ϖ ^ k})) (ϖ ^ k)
Tactic: rw [OrderDual.toDual_inj, ENat.recTopCoe_coe, hϖ.maximalIdeal_eq,
        span_singleton_pow, ← hϖ.addVal_pow k, addVal_eq_iff_associated]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞
⊢ 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 : ℕ∞ᵒᵈ)
have 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 : ℕ∞) → ℕ∞ᵒᵈ) ⊤ : ℕ∞ᵒᵈ)
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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞) → ℕ∞ᵒᵈ) ⊤ : ℕ∞ᵒᵈ)
⊢ 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 : ℕ∞ᵒᵈ)
have 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 : ℕ∞) : ℕ∞ᵒᵈ)
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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq (α := Ideal R) ((OrderIso.symm (idealOrderIsoENat R) : (a : ℕ∞ᵒᵈ) → Ideal R) (↑n : ℕ∞ᵒᵈ) : Ideal R)
    (span {ϖ ^ n} : Ideal R)
have rw : HPow.hPow (α := Ideal R) (maximalIdeal R) n = span {ϖ ^ n}
Tactic: rw [idealOrderIsoENat_symm_apply_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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}
⊢ Eq (α := Ideal R) ((OrderIso.symm (idealOrderIsoENat R) : (a : ℕ∞ᵒᵈ) → Ideal R) (↑n : ℕ∞ᵒᵈ) : Ideal R)
    (span {ϖ ^ n} : Ideal R)
have rw₁ : HPow.hPow (α := Ideal R) (span {ϖ}) n = span {ϖ ^ n}
Tactic: rw [idealOrderIsoENat_symm_apply_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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}
⊢ Eq (α := Ideal R) ((OrderIso.symm (idealOrderIsoENat R) : (a : ℕ∞ᵒᵈ) → Ideal R) (↑n : ℕ∞ᵒᵈ) : Ideal R)
    (span {ϖ ^ n} : Ideal R)
have rw₂ : Eq (α := Ideal R) (span {ϖ ^ n}) (span {ϖ ^ n})
Tactic: rw [idealOrderIsoENat_symm_apply_coe, hϖ.maximalIdeal_eq, span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
n : ℕ
⊢ Module.length R (R ⧸ HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)
have rw : Order.coheight (HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)
Tactic: rw [Module.length_quotient, coheight_pow_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ Module.length R (R ⧸ HPow.hPow (α := Ideal R) (maximalIdeal R) n) = (↑n : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [Module.length_quotient, coheight_pow_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ x = 0
have obtain : ∀ (ϖ : R) (hϖ : Irreducible ϖ), x = 0
Tactic: obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 ϖ
⊢ x = 0
have hx₁ : ∀ (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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞)
⊢ x = 0
have rwa : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)
Tactic: rwa [← addVal_eq_top_iff, WithTop.eq_top_iff_forall_ge]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞) (⊤ : ℕ∞)
⊢ x = 0
have rwa₁ : ∀ (b : ℕ), (↑b : WithTop ℕ) ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
Tactic: rwa [← addVal_eq_top_iff, WithTop.eq_top_iff_forall_ge]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
⊢ ⊥ < toWithBotNat x ↔ x ≠ 0
have rw : toWithBotNat x ≠ ⊥ ↔ x ≠ 0
Tactic: rw [bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ LE.le (α := WithBot ℕ) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞)
      (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ↔
    x ∣ y
have generalize : ∀ (vx : ℕ∞) (hvx : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x = vx),
  vx ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y ↔ x ∣ y
Tactic: generalize hvx : addVal R x = vx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
⊢ vx ≤ ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y ↔ x ∣ y
have generalize : ∀ (vy : ℕ∞) (hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy), vx ≤ vy ↔ x ∣ y
Tactic: generalize hvy : addVal R y = vy
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 : ℕ∞) (⊤ : ℕ∞)
⊢ ⊤ ≤ vy ↔ x ∣ y
have hvx₁ : x = 0
Tactic: rw [addVal_eq_top_iff] at hvx
Cleared hypotheses: hvx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 : ℕ∞) (⊤ : ℕ∞)
⊢ LE.le (α := WithBot ℕ) (↑vx : ℕ∞) ⊤ ↔ x ∣ y
have hvy₁ : y = 0
Tactic: rw [addVal_eq_top_iff] at hvy
Cleared hypotheses: hvy
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 : ℕ∞) ↔ x ∣ y
have coe : LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ LE.le (α := ℕ∞) (↑vx : ℕ∞) (↑vy : ℕ∞)
Tactic: rw [← addVal_le_iff_dvd, hvx, hvy]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
⊢ (↑vx : ℕ∞) ≤ vy ↔ x ∣ y
have coe : ∀ (hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) (⊤ : ℕ∞)),
  LE.le (α := WithBot ℕ) (↑vx : ℕ∞) ⊤ ↔ x ∣ y
Tactic: cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm
Cleared hypotheses: vy, hvy
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
vx : ℕ
hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)
coe :
  ∀ (hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) (⊤ : ℕ∞)),
    LE.le (α := WithBot ℕ) (↑vx : ℕ∞) ⊤ ↔ x ∣ y
⊢ (↑vx : ℕ∞) ≤ vy ↔ x ∣ y
have coe₁ : ∀ (vy : ℕ) (hvy : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y : ℕ∞) ((↑vy : ℕ∞) : ℕ∞)),
  LE.le (α := WithBot ℕ) (↑vx : ℕ∞) (↑vy : ℕ∞) ↔ x ∣ y
Tactic: cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm
Cleared hypotheses: vy, hvy
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
⊢ vx ≤ vy ↔ x ∣ y
have top : ∀ (hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)), ⊤ ≤ vy ↔ x ∣ y
Tactic: cases vx with
  | top => rw [addVal_eq_top_iff] at hvx; tauto
  | coe vx =>
    cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm
Cleared hypotheses: vx, hvx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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
vy : ℕ∞
hvy : ((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y = vy
top : ∀ (hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) (⊤ : ℕ∞)), ⊤ ≤ vy ↔ x ∣ y
⊢ vx ≤ vy ↔ x ∣ y
have coe : ∀ (vx : ℕ) (hvx : Eq (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x : ℕ∞) ((↑vx : ℕ∞) : ℕ∞)),
  (↑vx : ℕ∞) ≤ vy ↔ x ∣ y
Tactic: cases vx with
  | top => rw [addVal_eq_top_iff] at hvx; tauto
  | coe vx =>
    cases vy with
    | top => rw [addVal_eq_top_iff] at hvy; tauto
    | coe vy =>
      rw [← addVal_le_iff_dvd, hvx, hvy]
      exact WithBot.coe_le_coe.trans WithTop.coe_le_coe.symm
Cleared hypotheses: vx, hvx
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
⊢ x ∣ y
have pos : ∀ (hy : y = 0), x ∣ y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hle : toWithBotNat x ≤ toWithBotNat y
pos : ∀ (hy : y = 0), x ∣ y
⊢ x ∣ y
have neg : ∀ (hy : ¬y = 0), x ∣ y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
⊢ y * quotient x y + remainder x y = x
have rw : ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
    if y ∣ x then 0 else x) =
  x
Tactic: rw [remainder, quotient]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x
have pos : ∀ (h₁ : y = 0) (h₂ : y ∣ x), y * 0 + 0 = x
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
pos : ∀ (h₁ : y = 0) (h₂ : y ∣ x), y * 0 + 0 = x
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x
have neg : ∀ (h₁ : y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
pos : ∀ (h₁ : y = 0) (h₂ : y ∣ x), y * 0 + 0 = x
neg : ∀ (h₁ : y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x
have pos₁ : ∀ (h₁ : ¬y = 0) (h₂ : y ∣ x), y * Exists.choose (p := fun (c : R) ↦ x = y * c) h₂ + 0 = x
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
pos : ∀ (h₁ : y = 0) (h₂ : y ∣ x), y * 0 + 0 = x
neg : ∀ (h₁ : y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
pos₁ : ∀ (h₁ : ¬y = 0) (h₂ : y ∣ x), y * Exists.choose (p := fun (c : R) ↦ x = y * c) h₂ + 0 = x
⊢ ((y * if y = 0 then 0 else if h : y ∣ x then Exists.choose (p := fun (c : R) ↦ x = y * c) h else 0) +
      if y ∣ x then 0 else x) =
    x
have neg₁ : ∀ (h₁ : ¬y = 0) (h₂ : ¬y ∣ x), y * 0 + x = x
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (hypothesis)
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 y : R
h₁ : y = 0
h₂ : y ∣ x
⊢ y * 0 + 0 = x
have h₃ : x = 0
Tactic: rw [h₁, zero_dvd_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
h₁ : y = 0
h₂ : x = 0
⊢ y * 0 + 0 = x
have pos : HMul.hMul (α := R) 0 0 + 0 = 0
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
h₁ : y = 0
h₂ : ¬y ∣ x
⊢ y * 0 + x = x
have neg : HMul.hMul (α := R) 0 0 + x = x
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.Basic (goal)
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 y : R
h₁ : ¬y = 0
h₂ : y ∣ x
⊢ y * Exists.choose (p := fun (c : R) ↦ x = y * c) h₂ + 0 = x
have pos : x + 0 = x
Tactic: rw [← h₂.choose_spec]