awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ ∃ (r : R) (s : R),
    LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
have right : HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
  (↑γ : ValueGroup₀ v)
Tactic: use x, a, hx, zero_lt_iff.mpr ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ v)
have ha0 : Ne.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
  (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
Tactic: have ha0 : v.restrict a ≠ 0 := by simp [ha]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
ha0 :
  Ne.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ v)
have right : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) =
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
    ((embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
Tactic: rw [div_eq_iff ha0, mul_comm, ← embedding_strictMono.injective.eq_iff, map_mul,
    embedding_restrict, embedding_restrict, ← hax]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
ha0 :
  Ne.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) =
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
      ((embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
have right : (↑(↑u : Γ₀ˣ) : Γ₀) = (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
u : ↥(valueGroup v) := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
x : R
hax : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (v : (a : R) → Γ₀) x
hx : LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
ha0 :
  Ne.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ (↑(↑u : Γ₀ˣ) : Γ₀) = (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v)
have right : (↑(↑u : Γ₀ˣ) : Γ₀) =
  (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑(WithZero.unzero sorry) : WithZero ↥(valueGroup v))
Tactic: rw [← WithZero.coe_unzero (Units.ne_zero γ)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀ˣ
x_1 : R
x_in : Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} x_1
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} (-x_1)
have rwa : (v : (a : R) → Γ₀) (-x_1) < (↑γ : Γ₀)
Tactic: rwa [Set.mem_setOf, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v_1 : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀ˣ
x_1 : R
x_in : Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} x_1
rwa : (v : (a : R) → Γ₀) (-x_1) < (↑γ : Γ₀)
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} (-x_1)
have rwa₁ : (v : (a : R) → Γ₀) x_1 < (↑γ : Γ₀)
Tactic: rwa [Set.mem_setOf, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst_1 : Field K
v : Valuation K Γ₀
⊢ v.leAddSubgroup 0 = ⊥
have h : ∀ (x : K), x ∈ v.leAddSubgroup 0 ↔ Membership.mem (γ := AddSubgroup K) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
⊢ Nontrivial Γ₀
have obtain : ∀ (x : R) (hx0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (hx1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)), Nontrivial Γ₀
Tactic: obtain ⟨x, hx0, hx1⟩ := hv.exists_val_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : IsDomain R
inst_3 : DecidablePred fun (x : R) ↦ x = 0
x : R
hx : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx' : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ False
have inl : ∀ (hx : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (0 : Γ₀))
  (hx' : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (1 : Γ₀)), False
Tactic: rcases eq_or_ne x 0 with rfl | hx0
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : IsDomain R
inst_3 : DecidablePred fun (x : R) ↦ x = 0
x : R
hx : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx' : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
inl :
  ∀ (hx : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (0 : Γ₀))
    (hx' : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (1 : Γ₀)), False
⊢ False
have inr : ∀ (hx0 : x ≠ 0), False
Tactic: rcases eq_or_ne x 0 with rfl | hx0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueMonoid v)
have obtain : ∀ (x : R) (h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)),
  Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueMonoid v)
Tactic: obtain ⟨x, h0, h1⟩ := hv.exists_val_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueMonoid v)
have rw : ∃ (x : Γ₀ˣ), Membership.mem (γ := Submonoid Γ₀ˣ) (MonoidWithZeroHom.valueMonoid v) x ∧ x ≠ 1
Tactic: rw [Submonoid.nontrivial_iff_exists_ne_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : Γ₀ˣ), Membership.mem (γ := Submonoid Γ₀ˣ) (MonoidWithZeroHom.valueMonoid v) x ∧ x ≠ 1
have right : Ne.{u_7 + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : R) → Γ₀) x) h0 : Γ₀ˣ) (1 : Γ₀ˣ)
Tactic: use (Units.mk0 (v x) h0), MonoidWithZeroHom.mem_valueMonoid v (Set.mem_range_self x)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueGroup v)
have obtain : ∀ (x : R) (h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)), Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueGroup v)
Tactic: obtain ⟨x, h0, h1⟩ := hv.exists_val_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueGroup v)
have rw : ∃ (x : Γ₀ˣ), Membership.mem (γ := Subgroup Γ₀ˣ) (MonoidWithZeroHom.valueGroup v) x ∧ x ≠ 1
Tactic: rw [Subgroup.nontrivial_iff_exists_ne_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀_1
v_1 : Valuation R Γ₀_1
Γ₀ : Type u_7
inst_3 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
h0 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h1 : Ne.{u_7 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : Γ₀ˣ), Membership.mem (γ := Subgroup Γ₀ˣ) (MonoidWithZeroHom.valueGroup v) x ∧ x ≠ 1
have right : Ne.{u_7 + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : R) → Γ₀) x) h0 : Γ₀ˣ) (1 : Γ₀ˣ)
Tactic: use (Units.mk0 (v x) h0), MonoidWithZeroHom.mem_valueGroup v (Set.mem_range_self x)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have obtain : ∀ (x : Kˣ) (hx : Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)),
  ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: obtain ⟨x, hx⟩ := isNontrivial_iff_exists_unit.mp hv
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have hx₁ : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀) ∨
  LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
Tactic: rw [ne_iff_lt_or_gt] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx :
  LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inl : ∀ (hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)),
  ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx :
  LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
inl :
  ∀ (hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)),
    ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inr : ∀ (hx : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)),
  ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have h : (↑x : K) ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
Tactic: use x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have h : (↑x : K)⁻¹ ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K)⁻¹ : Γ₀) (1 : Γ₀)
Tactic: use x⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have obtain : ∀ (x : K) (h0 : x ≠ 0) (h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
  ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: obtain ⟨x, h0, h1⟩ := hv.exists_lt_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : K
h0 : x ≠ 0
h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have h : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀)
Tactic: use x⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst_1 : CommSemiring A
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ₀
inst_4 : IsTrivialOn A v
a : A
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
have pos : a = 0 → LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst_1 : CommSemiring A
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ₀
inst_4 : IsTrivialOn A v
a : A
pos : a = 0 → LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
have neg : ¬a = 0 → LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v v' : Valuation R Γ₀
h : v = v'
⊢ v.IsEquiv v'
have subst : v.IsEquiv v
Tactic: subst h
Cleared hypotheses: v', h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
inf : Injective.{u_4 + 1, u_5 + 1} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
h : v.IsEquiv v'
H : StrictMono.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀) := ⋯
r s : R
⊢ LE.le.{u_5} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ((v : (a : R) → Γ₀) r : Γ₀) : Γ'₀)
      ((f : (a : Γ₀) → Γ'₀) ((v : (a : R) → Γ₀) s : Γ₀) : Γ'₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ↔
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀)
Tactic: rw [H.le_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
inf : Injective.{u_4 + 1, u_5 + 1} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
h : v.IsEquiv v'
H : StrictMono.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀) := ⋯
r s : R
⊢ LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ((v' : (a : R) → Γ₀) r : Γ₀) : Γ'₀)
      ((f : (a : Γ₀) → Γ'₀) ((v' : (a : R) → Γ₀) s : Γ₀) : Γ'₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀) ↔
  LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀)
Tactic: rw [H.le_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
have this : Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) 0 : Γ₀) ↔
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)
Tactic: have : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0 := h.eq_iff
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) 0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
have rwa : ∀
  (this :
    Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
Tactic: rwa [v₁.map_zero, v₂.map_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) 0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)
rwa :
  ∀
    (this :
      Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
have rwa₁ : ∀
  (this :
    Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
Tactic: rwa [v₁.map_zero, v₂.map_zero] at this
Cleared hypotheses: this