awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (hypothesis)
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 ℤ))
⊢ (v : (a : R) → WithZero (Multiplicative ℤ)) x =
    (↑(HPow.hPow (β := ℤ) (generator v) (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
      WithZero (Multiplicative ℤ))
have hg : generator v = Units.mk0 (exp (-1)) sorry
Tactic: have hg : hv.generator = Units.mk0 (WithZero.exp (-1 : ℤ) : ℤᵐ⁰) (by simp) :=
      generator_eq_exp_neg_one_of_surjective hsurj
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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)) ⋯
| (v : (a : R) → WithZero (Multiplicative ℤ)) x
have rw : (↑(unzero h0) : WithZero (Multiplicative ℤ))
Tactic: rw [← coe_unzero h0]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.RankOne (goal)
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)) ⋯
⊢ (v : (a : R) → WithZero (Multiplicative ℤ)) x =
    (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (β := ℤ) (Units.mk0 (exp (-1)) ⋯)
          (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
      WithZero (Multiplicative ℤ))
have neg : (↑(unzero h0) : WithZero (Multiplicative ℤ)) =
  (↑(HPow.hPow (α := (WithZero (Multiplicative ℤ))ˣ) (β := ℤ) (Units.mk0 (exp (-1)) sorry)
        (-(Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero h0) : ℤ)) :
    WithZero (Multiplicative ℤ))
Tactic: conv_lhs => rw [← coe_unzero h0]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
have mp : Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) →
  IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
have mpr : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R) →
  Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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))
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := by simp [x]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
have hx1 : x < 1
Tactic: have hx1 : x < 1 := by simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
have mp : ∀ (y : ValueGroupWithZero R) (hy : y < 1), y ≤ x
Tactic: refine ⟨⟨x, hx1, fun y hy ↦ ?_⟩, ⟨x, hx0, hx1.ne⟩, .comap e.toMonoidHom e.strictMono⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ y ≤ x
have mp : ∀ (hy : LT.lt.{u_1} (α := ValueGroupWithZero R) 0 1), 0 ≤ x
Tactic: rcases eq_or_ne y 0 with rfl | hy0
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ y ≤ x
have mp₁ : ∀ (hy0 : y ≠ 0), y ≤ x
Tactic: rcases eq_or_ne y 0 with rfl | hy0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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
⊢ y ≤ x
have hy₁ : (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
Cleared hypotheses: hy, hy0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ y ≤ x
have mp : (EquivLike.inv e.symm y).log ≤ log (exp (-1))
Tactic: rw [← map_inv_le_iff, ← log_le_log (by simp [hy0]) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ LE.le (α := ℤ) (log ((e : (a : ValueGroupWithZero R) → WithZero (Multiplicative ℤ)) y)) (-1)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
hD : IsDiscrete R
hN : IsNontrivial R
hM : MulArchimedean.{u_1} (ValueGroupWithZero R)
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
have hN₁ : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
Tactic: rw [isNontrivial_iff_nontrivial_units] at hN
Cleared hypotheses: hN, hM
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ Nonempty.{max 1 (u_1 + 1)} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
have mpr : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
Tactic: rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ False
have mpr : ∀ (x : ValueGroupWithZero R) (hx : x < 1) (hx' : ∀ δ < 1, δ ≤ x), False
Tactic: obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ False
have mpr : ∀ (y : ValueGroupWithZero R) (hy : x < y) (hy' : y < 1), False
Tactic: obtain ⟨y, hy, hy'⟩ := exists_between hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
⊢ IsDiscrete R
have this : IsRankLeOne R
Tactic: have : IsRankLeOne R := .of_compatible_mulArchimedean v
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
⊢ IsDiscrete R
have pos : ∀ (h : IsNontrivial R), IsDiscrete R
Tactic: by_cases h : IsNontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ IsDiscrete R
have neg : ∀ (h : ¬IsNontrivial R), IsDiscrete R
Tactic: by_cases h : IsNontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ IsDiscrete R
have pos : ∀ (H : DenselyOrdered.{u_1} (ValueGroupWithZero R)), IsDiscrete R
Tactic: by_cases H : DenselyOrdered (ValueGroupWithZero R)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
⊢ IsDiscrete R
have neg : ∀ (H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)), IsDiscrete R
Tactic: by_cases H : DenselyOrdered (ValueGroupWithZero R)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ IsDiscrete R
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
have pos : Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
  (Set.range (ι := ValueGroupWithZero R)
    (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
      (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
Tactic: refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
    (Set.range (ι := ValueGroupWithZero R)
      (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
        (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
have pos : DenselyOrdered
  (↑(Set.range (ι := ValueGroupWithZero R)
        (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
          (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
    Type)
Tactic: rw [← WithZero.denselyOrdered_set_iff_subsingleton]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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)
⊢ IsDiscrete R
have pos : False
Tactic: classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
have pos₁ : Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
  (Set.range (ι := ValueGroupWithZero R)
    (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
      (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
Tactic: classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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
pos₁ :
  Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
    (Set.range (ι := ValueGroupWithZero R)
      (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
        (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
⊢ IsDiscrete R
have pos₂ : DenselyOrdered
  (↑(Set.range (ι := ValueGroupWithZero R)
        (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
          (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
    Type)
Tactic: classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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)
⊢ IsDiscrete R
have h₁ : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
Tactic: rw [isNontrivial_iff_nontrivial_units] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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 : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ IsDiscrete R
have H₁ : Nonempty.{u_1 + 1} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Tactic: rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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 : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : Nonempty.{u_1 + 1} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
⊢ IsDiscrete R
have H₁ : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
Tactic: rw [nonempty_orderIso_withZeroMul_int_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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
⊢ IsDiscrete R
have h₁ : ¬Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
Tactic: rw [isNontrivial_iff_nontrivial_units] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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 : ¬Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R
have h₁ : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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 : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R
have neg : ∀ (y : ValueGroupWithZero R) (hy : y < 1), y ≤ 0
Tactic: refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (goal)
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 : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : y < 1
⊢ y ≤ 0
have neg : ∀ (hy : 0 < y), 1 ≤ y
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.DiscreteValuativeRel (hypothesis)
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 : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
⊢ 1 ≤ y
have this₁ : 1 = Units.mk0 y sorry
Tactic: have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ vK.IsEquiv (comap (algebraMap K A) vA)
have rw : ∀ {x : K},
  LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
Tactic: rw [isEquiv_iff_val_le_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
have simp_rw : x ∈ vK.integer ↔ Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
Tactic: simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
simp_rw : x ∈ vK.integer ↔ Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
⊢ LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
have simp_rw₁ : Membership.mem (γ := Subring K) (Subring.comap (algebraMap K A) vA.integer) x ↔
  Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
Tactic: simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Extension (goal)
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
simp_rw : x ∈ vK.integer ↔ Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₁ :
  Membership.mem (γ := Subring K) (Subring.comap (algebraMap K A) vA.integer) x ↔
    Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
⊢ LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
have simp_rw₂ : Membership.mem (α := A) vA.integer (((algebraMap K A : K →+* A) : (a : K) → A) x : A) ↔
  Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
Tactic: simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]