awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
neg :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑(↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑(↑((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0)) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := ↥(valueGroup v))
    (Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
        Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
        (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯ :
      ↥(valueGroup v))
    ((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0) :
      ↥(valueGroup v))

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
neg :
  (v : (a : R) → WithZero (Multiplicative ℤ)) x =
    (↑(HPow.hPow (β := ℤ) (generator v) (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑(↑(Subtype.mk (p := fun (x : (WithZero (Multiplicative ℤ))ˣ) ↦
                Membership.mem (γ := Subgroup (WithZero (Multiplicative ℤ))ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → WithZero (Multiplicative ℤ)) x) h0) ⋯) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑(↑((intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯ : (a : Multiplicative ℤ) → ↥(valueGroup v)) (unzero h0)) :
            (WithZero (Multiplicative ℤ))ˣ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
simp only [Units.val_mk0, intEquivOfZPowersEqTop_apply, inv_zpow', generator',
      SubgroupClass.coe_zpow]

Premises used: SubgroupClass.coe_zpow, Valuation.IsRankOneDiscrete.generator', inv_zpow', intEquivOfZPowersEqTop_apply, Units.val_mk0
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ)) (exp (-1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ generator v = Units.mk0 (exp (-1)) ⋯

Tactic:
have hg : hv.generator = Units.mk0 (WithZero.exp (-1 : ℤ) : ℤᵐ⁰) (by simp) :=
      generator_eq_exp_neg_one_of_surjective hsurj
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
hg : generator v = Units.mk0 (exp (-1)) ⋯
rw : (↑(unzero h0) : WithZero (Multiplicative ℤ))
| (v : (a : R) → WithZero (Multiplicative ℤ)) x

Tactic:
rw [← coe_unzero h0]

Premises used: WithZero.coe_unzero
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
hg : generator v = Units.mk0 (exp (-1)) ⋯
neg :
  (↑(unzero h0) : WithZero (Multiplicative ℤ)) =
    (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (β := ℤ) (Units.mk0 (exp (-1)) ⋯)
          (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ (v : (a : R) → WithZero (Multiplicative ℤ)) x =
    (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (β := ℤ) (Units.mk0 (exp (-1)) ⋯)
          (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
conv_lhs => rw [← coe_unzero h0]

Premises used: WithZero.coe_unzero
-- Module: Mathlib.RingTheory.Valuation.Discrete.RankOne
Goal:
R : Type u_2
inst : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective (α := R) (β := WithZero (Multiplicative ℤ)) (⇑v : (a : R) → WithZero (Multiplicative ℤ))
x : R
h0 :
  ¬Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
hg : generator v = Units.mk0 (exp (-1)) ⋯
⊢ Eq (α := WithZero (Multiplicative ℤ)) ((v : (a : R) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
    (exp ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0)) : WithZero (Multiplicative ℤ))

Tactic:
simp [WithZero.exp]

Premises used: WithZero.exp
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
mp :
  Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) →
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
mpr :
  IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R) →
    Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
⊢ x ≠ 0

Tactic:
simp [x]
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := by simp [x]
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
⊢ x < 1

Tactic:
simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]

Premises used: lt_map_inv_iff, WithZero.exp_zero, WithZero.exp_neg
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
⊢ x < 1

Tactic:
have hx1 : x < 1 := by simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
⟨⟨x, hx1, fun y hy ↦ ?_⟩, ⟨x, hx0, hx1.ne⟩, .comap e.toMonoidHom e.strictMono⟩

Premises used: ValuativeRel.IsDiscrete.mk, ValuativeRel.IsNontrivial.mk, MulEquiv.toMonoidHom, MulArchimedean.comap, And.intro, OrderMonoidIso.strictMono, Exists.intro, OrderMonoidIso.toMulEquiv, LT.lt.ne
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
mp : ∀ (y : ValueGroupWithZero R) (hy : y < 1), y ≤ x
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
refine ⟨⟨x, hx1, fun y hy ↦ ?_⟩, ⟨x, hx0, hx1.ne⟩, .comap e.toMonoidHom e.strictMono⟩
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
mp : ∀ (hy : LT.lt.{u_1} (α := ValueGroupWithZero R) 0 1), 0 ≤ x
mp₁ : ∀ (hy0 : y ≠ 0), y ≤ x
⊢ y ≤ x

Tactic:
rcases eq_or_ne y 0 with rfl | hy0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
hy : LT.lt.{u_1} (α := ValueGroupWithZero R) 0 1
⊢ 0 ≤ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : EquivLike.inv e.symm y < 1
hy0 : y ≠ 0
⊢ EquivLike.inv e.symm y ≠ 0

Tactic:
simp [hy0]
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : EquivLike.inv e.symm y < 1
hy0 : y ≠ 0
⊢ Ne (α := WithZero (Multiplicative ℤ)) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
hy0 : y ≠ 0
⊢ (EquivLike.inv e.symm y).log < log 1

Tactic:
rw [← map_one e.symm, ← map_inv_lt_iff, ← log_lt_log (by simp [hy0]) (by simp)] at hy

Premises used: WithZero.log_lt_log, map_one, map_inv_lt_iff, OrderMonoidIso.symm
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
hy0 : y ≠ 0
hy₁ : (EquivLike.inv e.symm y).log < log 1
⊢ y ≠ 0

Tactic:
rw [← map_one e.symm, ← map_inv_lt_iff, ← log_lt_log (by simp [hy0]) (by simp)] at hy

Premises used: WithZero.log_lt_log, map_one, map_inv_lt_iff, OrderMonoidIso.symm
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : (EquivLike.inv e.symm y).log < log 1
hy0 : y ≠ 0
⊢ EquivLike.inv e.symm y ≠ 0

Tactic:
simp [hy0]
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : (EquivLike.inv e.symm y).log < log 1
hy0 : y ≠ 0
⊢ Ne (α := WithZero (Multiplicative ℤ)) (exp (-1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : (EquivLike.inv e.symm y).log < log 1
hy0 : y ≠ 0
mp : (EquivLike.inv e.symm y).log ≤ log (exp (-1))
⊢ y ≤ x

Tactic:
rw [← map_inv_le_iff, ← log_le_log (by simp [hy0]) (by simp)]

Premises used: WithZero.log_le_log, map_inv_le_iff
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := (e.symm : (a : WithZero (Multiplicative ℤ)) → ValueGroupWithZero R) (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : LT.lt (α := ℤ) (log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) 0
hy0 : y ≠ 0
linarith :
  LT.lt (α := ℤ) (-1) (log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) →
    -1 + (HAdd.hAdd (α := ℤ) (log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) 1 - 0) +
        (HAdd.hAdd (α := ℤ) (-1) 1 - log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) =
      0
⊢ LE.le (α := ℤ) (log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) (-1)

Tactic:
linarith
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : IsNontrivial R
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
⊢ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
rw [isNontrivial_iff_nontrivial_units] at hN

Premises used: ValuativeRel.isNontrivial_iff_nontrivial_units
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : IsNontrivial R
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
hN₁ : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
⊢ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
rw [isNontrivial_iff_nontrivial_units] at hN

Premises used: ValuativeRel.isNontrivial_iff_nontrivial_units
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
mpr : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]

Premises used: LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
mpr : ∀ (x : ValueGroupWithZero R) (hx : x < 1) (hx' : ∀ δ < 1, δ ≤ x), False
⊢ False

Tactic:
obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element

Premises used: ValuativeRel.IsDiscrete.has_maximal_element
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
mpr : ∀ (y : ValueGroupWithZero R) (hy : x < y) (hy' : y < 1), False
⊢ False

Tactic:
obtain ⟨y, hy, hy'⟩ := exists_between hx

Premises used: exists_between
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
y : ValueGroupWithZero R
hy : x < y
hy' : y < 1
⊢ False

Tactic:
hy.not_ge (hx' y hy')

Premises used: LT.lt.not_ge
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
y : ValueGroupWithZero R
hy : x < y
hy' : y < 1
⊢ False

Tactic:
exact hy.not_ge (hx' y hy')

Premises used: LT.lt.not_ge
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
⊢ IsRankLeOne R

Tactic:
have : IsRankLeOne R := .of_compatible_mulArchimedean v
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
pos : ∀ (h : IsNontrivial R), IsDiscrete R
neg : ∀ (h : ¬IsNontrivial R), IsDiscrete R
⊢ IsDiscrete R

Tactic:
by_cases h : IsNontrivial R

Premises used: ValuativeRel.IsNontrivial
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
pos : ∀ (H : DenselyOrdered.{u_1} (ValueGroupWithZero R)), IsDiscrete R
neg : ∀ (H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)), IsDiscrete R
⊢ IsDiscrete R

Tactic:
by_cases H : DenselyOrdered (ValueGroupWithZero R)

Premises used: DenselyOrdered, ValuativeRel.ValueGroupWithZero
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
pos : False
⊢ IsDiscrete R

Tactic:
exfalso
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ False

Tactic:
(MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_

Premises used: MonoidWithZeroHom.range_nontrivial, ValuativeRel.ValueGroupWithZero.orderMonoidIso, Set.Nontrivial.not_subsingleton, OrderMonoidIso.toMulEquiv, MulEquiv.toMonoidWithZeroHom
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
pos :
  Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
    (Set.range (ι := ValueGroupWithZero R)
      (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
        (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
⊢ False

Tactic:
refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_

Premises used: MonoidWithZeroHom.range_nontrivial, ValuativeRel.ValueGroupWithZero.orderMonoidIso, Set.Nontrivial.not_subsingleton, OrderMonoidIso.toMulEquiv, MulEquiv.toMonoidWithZeroHom
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
pos :
  DenselyOrdered
    (↑(Set.range (ι := ValueGroupWithZero R)
          (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
            (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
      Type)
⊢ Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
    (Set.range (ι := ValueGroupWithZero R)
      (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
        (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))

Tactic:
rw [← WithZero.denselyOrdered_set_iff_subsingleton]

Premises used: WithZero.denselyOrdered_set_iff_subsingleton
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ DenselyOrdered
    (↑(Set.range (ι := ValueGroupWithZero R)
          (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
            (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
      Type)

Tactic:
(ValueGroupWithZero.embed_strictMono v).denselyOrdered_range

Premises used: Set.Mem, ValuativeRel.ValueGroupWithZero.embed_strictMono, ValuativeRel.ValueGroupWithZero.lift, StrictMono.denselyOrdered_range
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ DenselyOrdered
    (↑(Set.range (ι := ValueGroupWithZero R)
          (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
            (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
      Type)

Tactic:
exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range

Premises used: ValuativeRel.ValueGroupWithZero.embed_strictMono, StrictMono.denselyOrdered_range