awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : @vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have neg : @vle _ inst _ y 0
Tactic: absurd hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : @vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ @vle _ inst _ y 0
have neg : @vle _ inst _ (y * (↑s : R)) (0 * (↑s : R))
Tactic: apply vle_mul_cancel s.prop
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : @vle _ inst _ y 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have pos : @vle _ inst _ x 0
Tactic: absurd hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : @vle _ inst _ y 0
⊢ @vle _ inst _ x 0
have pos : @vle _ inst _ (x * (↑t : R)) (0 * (↑t : R))
Tactic: apply vle_mul_cancel t.prop
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      x s)
    ((fun (x : R) (s : ↥(posSubmonoid R)) ↦
        (if h : @vle _ inst _ x 0 then 0
          else
            ValueGroupWithZero.mk (↑s : R)
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) :
          ValueGroupWithZero R))
      y t)
have neg : Eq (α := ValueGroupWithZero R)
  (ValueGroupWithZero.mk (↑s : R)
    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx))
  (ValueGroupWithZero.mk (↑t : R)
    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy))
Tactic: simp only [dif_neg hx, dif_neg hy]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
⊢ Eq (α := ValueGroupWithZero R)
    (ValueGroupWithZero.mk (↑s : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx))
    (ValueGroupWithZero.mk (↑t : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy))
have neg : @vle _ inst _
  ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
  ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
Tactic: apply ValueGroupWithZero.sound
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x y : R
t s : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
hx : ¬@vle _ inst _ x 0
hy : ¬@vle _ inst _ y 0
neg :
  @vle _ inst _
    ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
    ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
⊢ Eq (α := ValueGroupWithZero R)
    (ValueGroupWithZero.mk (↑s : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx))
    (ValueGroupWithZero.mk (↑t : R)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy))
have neg₁ : @vle _ inst _
  ((↑t : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x hx) : R))
  ((↑s : R) * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) y hy) : R))
Tactic: apply ValueGroupWithZero.sound
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
⊢ ∃ (x : ValueGroupWithZero R) (y : ValueGroupWithZero R), x ≠ y
have refine : ∀ (h : Eq.{u_1 + 1} (α := ValueGroupWithZero R) 0 1), False
Tactic: refine ⟨0, 1, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : Eq.{u_1 + 1} (α := ValueGroupWithZero R) 0 1
⊢ False
have h₁ : LE.le.{u_1} (α := ValueGroupWithZero R) 1 0
Tactic: apply ge_of_eq at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : LE.le.{u_1} (α := ValueGroupWithZero R) 1 0
⊢ False
have h₁ : @vle _ inst _ (HMul.hMul (α := R) 1 (↑1 : R)) (HMul.hMul (α := R) 0 (↑1 : R))
Tactic: rw [← ValueGroupWithZero.mk_zero 1, ← ValueGroupWithZero.mk_one_one,
      ValueGroupWithZero.mk_le_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ValueGroupWithZero.mk x y ≠ 0
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
have h₁ : ¬(@vle _ inst _ (x * (↑1 : R)) (0 * (↑y : R)) ∧ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R)))
Tactic: rw [ne_eq, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_eq_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ¬(@vle _ inst _ (x * (↑1 : R)) (0 * (↑y : R)) ∧ @vle _ inst _ (0 * (↑y : R)) (x * (↑1 : R)))
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
have h₁ : ¬@vle _ inst _ x 0
Tactic: simp only [Submonoid.coe_one, mul_one, zero_mul, zero_vle, and_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z x : R
y : ↥(posSubmonoid R)
h : ¬@vle _ inst _ x 0
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
have rw : @vle _ inst _ (x * (↑y : R) * (↑1 : R))
    (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R)) ∧
  @vle _ inst _
    (1 * (↑(y * Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (posSubmonoid R) x) x h) : R))
    (x * (↑y : R) * (↑1 : R))
Tactic: rw [ValueGroupWithZero.inv_mk x y h, ← ValueGroupWithZero.mk_one_one,
      ValueGroupWithZero.mk_mul_mk, ValueGroupWithZero.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑x : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
have rw : ¬@vle _ inst _ (↑x : R) 0
Tactic: rw [ne_eq, valuation_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s =
    HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) r : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
have rw : HMul.hMul (β := ValueGroupWithZero R) (ValueGroupWithZero.mk r s)
    ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
  (valuation R : (a : R) → ValueGroupWithZero R) r
Tactic: rw [eq_div_iff (valuation_posSubmonoid_ne_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 : S
h_1 : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)
h : S
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * h) : Γ) ((v : (a : S) → Γ) (y_1 * h) : Γ)
have simp : HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) h : Γ) ≤
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) h : Γ)
Tactic: simp only [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) ((v : (a : S) → Γ) 0 : Γ)
h : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)
have h0₁ : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
Tactic: rw [map_zero, le_zero_iff] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
S : Type u_2
Γ : Type u_3
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
x_1 y_1 z_1 : S
h0 : ¬Eq.{u_3 + 1} (α := Γ) ((v : (a : S) → Γ) z_1 : Γ) (0 : Γ)
h : LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) (x_1 * z_1) : Γ) ((v : (a : S) → Γ) (y_1 * z_1) : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) y_1 : Γ)
have h₁ : HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) x_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ) ≤
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : S) → Γ) y_1 : Γ) ((v : (a : S) → Γ) z_1 : Γ)
Tactic: simp only [map_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x y : R
⊢ x =ᵥ y ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have simp_rw : @vle _ inst _ x y ∧ @vle _ inst _ y x ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: simp_rw [veq_def, vle_iff_le v, antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x y : R
simp_rw :
  @vle _ inst _ x y ∧ @vle _ inst _ y x ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ x =ᵥ y ↔ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have simp_rw₁ : LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ∧
    LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ↔
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
Tactic: simp_rw [veq_def, vle_iff_le v, antisymm_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ x <ᵥ y ↔ @vle _ inst _ x y ∧ ¬@vle _ inst _ y x
have this : @vle _ inst _ x y ∨ @vle _ inst _ y x
Tactic: have := vle_total x y
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Eq (α := Ideal R) (supp R) (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R))
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (supp R) x ↔
    Membership.mem (γ := Ideal R) (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Ideal.IsPrime (supp R)
have rw : Ideal.IsPrime (Valuation.supp (Γ₀ := ValueGroupWithZero R) (valuation R))
Tactic: rw [supp_eq_valuation_supp]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : @vle _ inst _ a b
n : ℕ
⊢ @vle _ inst _ (a ^ n) (b ^ n)
have zero : @vle _ inst _ (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)
Tactic: induction n with
  | zero => simp
  | succ _ hn => simp [pow_succ, mul_vle_mul hn hab]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : @vle _ inst _ a b
n : ℕ
zero : @vle _ inst _ (HPow.hPow (β := ℕ) a 0) (HPow.hPow (β := ℕ) b 0)
⊢ @vle _ inst _ (a ^ n) (b ^ n)
have succ : ∀ (n : ℕ) (hn : @vle _ inst _ (a ^ n) (b ^ n)), @vle _ inst _ (a ^ (n + 1)) (b ^ (n + 1))
Tactic: induction n with
  | zero => simp
  | succ _ hn => simp [pow_succ, mul_vle_mul hn hab]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
n : ℕ
hn : n ≠ 0
⊢ a ^ n <ᵥ b ^ n
have zero : ∀ (hn : Ne (α := ℕ) 0 0), HPow.hPow (β := ℕ) a 0 <ᵥ HPow.hPow (β := ℕ) b 0
Tactic: induction n using Nat.twoStepInduction with
  | zero => contradiction
  | one => simpa
  | more _ _ => simp_all [pow_succ, mul_vlt_mul]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), HPow.hPow (β := ℕ) a 0 <ᵥ HPow.hPow (β := ℕ) b 0
⊢ a ^ n <ᵥ b ^ n
have one : ∀ (hn : Ne (α := ℕ) 1 0), HPow.hPow (β := ℕ) a 1 <ᵥ HPow.hPow (β := ℕ) b 1
Tactic: induction n using Nat.twoStepInduction with
  | zero => contradiction
  | one => simpa
  | more _ _ => simp_all [pow_succ, mul_vlt_mul]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a b : R
hab : a <ᵥ b
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), HPow.hPow (β := ℕ) a 0 <ᵥ HPow.hPow (β := ℕ) b 0
one : ∀ (hn : Ne (α := ℕ) 1 0), HPow.hPow (β := ℕ) a 1 <ᵥ HPow.hPow (β := ℕ) b 1
⊢ a ^ n <ᵥ b ^ n
have more : ∀ (n : ℕ),
  (∀ (hn : n ≠ 0), a ^ n <ᵥ b ^ n) →
    (∀ (hn : n + 1 ≠ 0), a ^ (n + 1) <ᵥ b ^ (n + 1)) → ∀ (hn : n + 2 ≠ 0), a ^ (n + 2) <ᵥ b ^ (n + 2)
Tactic: induction n using Nat.twoStepInduction with
  | zero => contradiction
  | one => simpa
  | more _ _ => simp_all [pow_succ, mul_vlt_mul]
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ a 1
n m : ℕ
hnm : n ≤ m
⊢ @vle _ inst _ (a ^ m) (a ^ n)
have obtain : ∀ (m : ℕ) (hnm : n ≤ n + m), @vle _ inst _ (a ^ (n + m)) (a ^ n)
Tactic: obtain ⟨m, rfl⟩ := exists_add_of_le hnm
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : ValuativeRel R
a : R
ha : @vle _ inst _ 1 a
n m : ℕ
hnm : n ≤ m
⊢ @vle _ inst _ (a ^ n) (a ^ m)
have obtain : ∀ (m : ℕ) (hnm : n ≤ n + m), @vle _ inst _ (a ^ n) (a ^ (n + m))
Tactic: obtain ⟨m, rfl⟩ := exists_add_of_le hnm
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
⊢ @vle _ Field.toCommRing _ a 0 ↔ a = 0
have rw : Membership.mem (γ := Ideal K) (supp K) a ↔ a = 0
Tactic: rw [← supp_def, Ideal.eq_bot_of_prime (supp K), Ideal.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : Membership.mem (γ := Ideal K) (supp K) a ↔ a = 0
⊢ @vle _ Field.toCommRing _ a 0 ↔ a = 0
have rw₁ : Membership.mem (γ := Ideal K) ⊥ a ↔ a = 0
Tactic: rw [← supp_def, Ideal.eq_bot_of_prime (supp K), Ideal.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : Membership.mem (γ := Ideal K) (supp K) a ↔ a = 0
rw₁ : Membership.mem (γ := Ideal K) ⊥ a ↔ a = 0
⊢ @vle _ Field.toCommRing _ a 0 ↔ a = 0
have rw₂ : a = 0 ↔ a = 0
Tactic: rw [← supp_def, Ideal.eq_bot_of_prime (supp K), Ideal.mem_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
⊢ 0 =ᵥ a ↔ 0 = a
have rw : a =ᵥ 0 ↔ 0 = a
Tactic: rw [veq_comm, eq_comm, zero_veq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : a =ᵥ 0 ↔ 0 = a
⊢ 0 =ᵥ a ↔ 0 = a
have rw₁ : a =ᵥ 0 ↔ a = 0
Tactic: rw [veq_comm, eq_comm, zero_veq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a : K
rw : a =ᵥ 0 ↔ 0 = a
rw₁ : a =ᵥ 0 ↔ a = 0
⊢ 0 =ᵥ a ↔ 0 = a
have rw₂ : a = 0 ↔ a = 0
Tactic: rw [veq_comm, eq_comm, zero_veq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ @vle _ Field.toCommRing _ a (b / c) ↔ @vle _ Field.toCommRing _ (a * c) b
have rw : @vle _ Field.toCommRing _ (a * c) (b / c * c) ↔ @vle _ Field.toCommRing _ (a * c) b
Tactic: rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
rw : @vle _ Field.toCommRing _ (a * c) (b / c * c) ↔ @vle _ Field.toCommRing _ (a * c) b
⊢ @vle _ Field.toCommRing _ a (b / c) ↔ @vle _ Field.toCommRing _ (a * c) b
have rw₁ : @vle _ Field.toCommRing _ (a * c) b ↔ @vle _ Field.toCommRing _ (a * c) b
Tactic: rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
⊢ @vle _ Field.toCommRing _ (a / c) b ↔ @vle _ Field.toCommRing _ a (b * c)
have rw : @vle _ Field.toCommRing _ (a / c * c) (b * c) ↔ @vle _ Field.toCommRing _ a (b * c)
Tactic: rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
a b c : K
hc : c ≠ 0
rw : @vle _ Field.toCommRing _ (a / c * c) (b * c) ↔ @vle _ Field.toCommRing _ a (b * c)
⊢ @vle _ Field.toCommRing _ (a / c) b ↔ @vle _ Field.toCommRing _ a (b * c)
have rw₁ : @vle _ Field.toCommRing _ a (b * c) ↔ @vle _ Field.toCommRing _ a (b * c)
Tactic: rw [← mul_vle_mul_iff_left (by simpa), div_mul_cancel₀ _ (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
have obtain : ∀ (γ : ValueGroupWithZero R) (h0 : γ ≠ 0) (h1 : γ ≠ 1), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
Tactic: obtain ⟨γ, h0, h1⟩ := IsNontrivial.condition (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1 : γ ≠ 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
have inl : ∀ (h1 : γ < 1), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
Tactic: obtain h1 | h1 := lt_or_lt_iff_ne.mpr h1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsNontrivial R
γ : ValueGroupWithZero R
h0 : γ ≠ 0
h1 : γ ≠ 1
inl : ∀ (h1 : γ < 1), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
⊢ ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
have inr : ∀ (h1 : 1 < γ), ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1
Tactic: obtain h1 | h1 := lt_or_lt_iff_ne.mpr h1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ IsNontrivial R ↔ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
have mp : IsNontrivial R → Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
mp : IsNontrivial R → Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
⊢ IsNontrivial R ↔ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
have mpr : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ → IsNontrivial R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
hγ' : γ ≠ 1
⊢ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
have mp : Units.mk0 γ hγ ≠ 1
Tactic: refine ⟨Units.mk0 _ hγ, 1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
⊢ IsNontrivial R
have mpr : ∀ (h : 1 ≠ s), IsNontrivial R
Tactic: rcases eq_or_ne r 1 with rfl | hr
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
mpr : ∀ (h : 1 ≠ s), IsNontrivial R
⊢ IsNontrivial R
have mpr₁ : ∀ (hr : r ≠ 1), IsNontrivial R
Tactic: rcases eq_or_ne r 1 with rfl | hr