awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
inst_2 : v.IsNontrivial
⊢ ∃ (x : R),
    Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ∧
      Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have obtain : ∀ (x : R) (hx0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (hx1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)),
  ∃ (x : R),
    Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ∧
      Ne.{u_2 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: obtain ⟨x, ⟨hx0, hx1⟩⟩ := IsNontrivial.exists_val_nontrivial (v := v)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have hγ_pos : 0 < γ
Tactic: have hγ_pos : 0 < γ := pos_iff_ne_zero.mpr hγ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have obtain : ∀ (x : (ValueGroup₀ v.restrict)ˣ)
  (h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ),
  ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
Tactic: obtain ⟨x, h⟩ := NNReal.exists_lt_of_strictMono (RankOne.strictMono v.restrict) hγ_pos
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have obtain : ∀ (k : K)
  (hk :
    ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
          (a : K) → ValueGroup₀ v.restrict)
        k =
      (↑x : ValueGroup₀ v.restrict)),
  ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
Tactic: obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have refine_1 : k ≠ 0
Tactic: refine ⟨k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
refine_1 : k ≠ 0
⊢ ∃ (x : K), x ≠ 0 ∧ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have refine_2 : (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) < γ
Tactic: refine ⟨k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
h0 : k = 0
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
        WithZero ↥(valueGroup v)))
    0
have rw : Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) 0 0
Tactic: rw [dif_pos ((zero_iff v).mpr h0)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  (if h :
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
              WithZero ↥(valueGroup v)))
          0 then
      0
    else
      (↑(Subtype.mk (p := fun (x : (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) ↦
            Membership.mem (γ := Subgroup (ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))ˣ) (valueGroup v.restrict) x)
            (Units.mk0
              (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀) then 0
              else
                (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                      (Units.mk0 ((v : (a : K) → Γ₀) k) h) ⋯) :
                  WithZero ↥(valueGroup v)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup v.restrict))) =
    (↑x : ValueGroup₀ v.restrict)
h0 : k = 0
⊢ False
have hk₁ : (↑x : ValueGroup₀ v.restrict) = 0
Tactic: rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk
Cleared hypotheses: hk, h0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
⊢ (hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) < γ
have h₁ : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
  ((hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) : ℝ≥0)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) : ℝ≥0)
have h₁ : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
  ((hom v : (a : ValueGroup₀ v) → ℝ≥0)
      ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
        (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
              (a : K) → ValueGroup₀ v.restrict)
            k :
          ValueGroup₀ v.restrict)) :
    ℝ≥0)
Tactic: simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ValueGroup₀ v.restrict)ˣ
h : (hom v.restrict : (a : ValueGroup₀ v.restrict) → ℝ≥0) (↑x : ValueGroup₀ v.restrict) < γ
k : K
hk :
  ((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) : (a : K) → ValueGroup₀ v.restrict)
      k =
    (↑x : ValueGroup₀ v.restrict)
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k) : ℝ≥0)
    ((hom v : (a : ValueGroup₀ v) → ℝ≥0)
        ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
          (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
                (a : K) → ValueGroup₀ v.restrict)
              k :
            ValueGroup₀ v.restrict)) :
      ℝ≥0)
have h₁ : Eq.{u_2 + 1} (α := ValueGroup₀ v)
  ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) k : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  ((embedding : (a : ValueGroup₀ v.restrict) → ValueGroup₀ v)
      (((restrict₀ v.restrict : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v.restrict)) :
            (a : K) → ValueGroup₀ v.restrict)
          k :
        ValueGroup₀ v.restrict) :
    ValueGroup₀ v)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (x : K), x ≠ 0 ∧ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K),
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have by_contra! : ∀
  (H' :
    ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
      Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
  False
Tactic: by_contra! H'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (x : K), x ≠ 0 ∧ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False
have obtain : ∀ (x : K) (hx : x ≠ 0) (hx' : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)), False
Tactic: obtain ⟨x, hx, hx'⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : Nontrivial.{u_2} (ValueGroup₀ v)ˣ
⊢ ∃ (x : K),
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have by_contra! : ∀
  (H' :
    ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
      Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
  False
Tactic: by_contra! H'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : Nontrivial.{u_2} (ValueGroup₀ v)ˣ
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False
have H₁ : ∃ (y : (ValueGroup₀ v)ˣ), y ≠ 1
Tactic: rw [nontrivial_iff_exists_ne 1] at H
Cleared hypotheses: H, H'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H : ∃ (y : (ValueGroup₀ v)ˣ), y ≠ 1
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False
have obtain : ∀ (x : (ValueGroup₀ v)ˣ) (hx : x ≠ 1), False
Tactic: obtain ⟨x, hx⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
⊢ False
have obtain : ∀ (k : K)
  (hk :
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k =
      (↑x : ValueGroup₀ v)),
  False
Tactic: obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
have rw : ¬(↑x : ValueGroup₀ v) = 0
Tactic: rw [ne_eq, ← restrict₀_eq_zero_iff, hk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
⊢ False
have h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
Tactic: have h0 : v k ≠ 0 := by
      rw [ne_eq, ← restrict₀_eq_zero_iff, hk]
      simp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
⊢ Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)
have rw : ¬(↑x : ValueGroup₀ v) = 1
Tactic: rw [ne_eq, ← restrict₀_eq_one_iff, hk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_2 : DivisionRing K
v : Valuation K Γ₀
inst_3 : v.RankLeOne
H' :
  ∀ (x : K) (_ : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : (ValueGroup₀ v)ˣ
hx : x ≠ 1
k : K
hk : ((restrict₀ v : MonoidWithZeroHom.{u_3, u_2} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) k = (↑x : ValueGroup₀ v)
h0 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (0 : Γ₀)
⊢ False
have h1 : Ne.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) (1 : Γ₀)
Tactic: have h1 : v k ≠ 1 := by
      rw [ne_eq, ← restrict₀_eq_one_iff, hk]
      simp [hx]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_4
inst_1 : Field K
v : Valuation K Γ₀
inst_2 : v.RankLeOne
⊢ Subsingleton.{u_2 + 1} (ValueGroup₀ v)ˣ ∨
    ∀ {γ : ℝ≥0},
      γ ≠ 0 →
        ∃ (x : K),
          x ≠ 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
have simp : Nontrivial.{u_2} (ValueGroup₀ v)ˣ →
  ∀ {γ : ℝ≥0},
    ¬γ = 0 →
      ∃ (x : K),
        ¬x = 0 ∧ (hom' v : (a : ValueGroup₀ v) → ℝ≥0) ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x) < γ
Tactic: simp only [ne_eq, or_iff_not_imp_left, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
⊢ IsRankLeOne R ↔ MulArchimedean.{u_3} (ValueGroupWithZero R)
have mp : IsRankLeOne R → MulArchimedean.{u_3} (ValueGroupWithZero R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
mp : IsRankLeOne R → MulArchimedean.{u_3} (ValueGroupWithZero R)
⊢ IsRankLeOne R ↔ MulArchimedean.{u_3} (ValueGroupWithZero R)
have mpr : MulArchimedean.{u_3} (ValueGroupWithZero R) → IsRankLeOne R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
⊢ IsRankLeOne R
have pos : ∀ (H : IsNontrivial R), IsRankLeOne R
Tactic: by_cases H : IsNontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
pos : ∀ (H : IsNontrivial R), IsRankLeOne R
⊢ IsRankLeOne R
have neg : ∀ (H : ¬IsNontrivial R), IsRankLeOne R
Tactic: by_cases H : IsNontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : IsNontrivial R
⊢ IsRankLeOne R
have H₁ : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
Tactic: rw [isNontrivial_iff_isNontrivial (valuation R)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
⊢ IsRankLeOne R
have h' : MulArchimedean.{u_3} (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))
Tactic: have h' : MulArchimedean (ValueGroup₀ (valuation R)) :=
        MulArchimedean.comap embedding.toMonoidHom embedding_strictMono
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
h' : MulArchimedean.{u_3} (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))
⊢ IsRankLeOne R
have h'₁ : Nonempty.{u_3 + 1} (Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R))
Tactic: rw [← (valuation R).nonempty_rankOne_iff_mulArchimedean] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : Valuation.IsNontrivial (Γ₀ := ValueGroupWithZero R) (valuation R)
h' : Nonempty.{u_3 + 1} (Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R))
⊢ IsRankLeOne R
have pos : ∀ (f : Valuation.RankOne (Γ₀ := ValueGroupWithZero R) (valuation R)), IsRankLeOne R
Tactic: obtain ⟨f⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : ¬IsNontrivial R
⊢ IsRankLeOne R
have neg : StrictMono.{u_3, 0} (α := ValueGroupWithZero R) (β := ℝ≥0) (⇑1 : (a : ValueGroupWithZero R) → ℝ≥0)
Tactic: refine ⟨⟨{ emb := 1, strictMono := ?_ }⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
H : ¬IsNontrivial R
a b : ValueGroupWithZero R
⊢ a < b →
    LT.lt (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
have neg : ∀
  (H :
    a < b ∧
      LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
        (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)),
  IsNontrivial R
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
h : MulArchimedean.{u_3} (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H :
  a < b ∧
    LE.le (α := ℝ≥0) (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) b : ℝ≥0)
      (((1 : ValueGroupWithZero R →*₀ ℝ≥0) : (a : ValueGroupWithZero R) → ℝ≥0) a : ℝ≥0)
⊢ IsNontrivial R
have H₁ : a < b
Tactic: obtain ⟨H, H'⟩ := H
Cleared hypotheses: H