awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
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 ⋯
obtain :
  ∀ (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),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨a, ⟨ha, x, hax⟩⟩ := (mem_valueGroup_iff_of_comm _).mp u.2

Premises used: Iff.mp, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.Basic
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
rw : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]

Premises used: WithZero.pos_iff_ne_zero, MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq, Valuation.restrict_pos_iff, Valuation.restrict_def
-- Module: Mathlib.RingTheory.Valuation.Basic
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
⊢ ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Basic
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
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
have hx : 0 < v x := by
    rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
    aesop
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
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)
⊢ ∃ (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)

Tactic:
use x, a, hx, zero_lt_iff.mpr ha

Premises used: Iff.mpr, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
⊢ 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:
simp [ha]
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
⊢ 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]
-- Module: Mathlib.RingTheory.Valuation.Basic
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 →*₀ Γ₀))
right :
  HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) =
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
      ((embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ 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:
rw [div_eq_iff ha0, mul_comm, ← embedding_strictMono.injective.eq_iff, map_mul,
    embedding_restrict, embedding_restrict, ← hax]

Premises used: Function.Injective.eq_iff, Valuation.embedding_restrict, map_mul, StrictMono.injective, div_eq_iff, mul_comm
-- Module: Mathlib.RingTheory.Valuation.Basic
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 →*₀ Γ₀))
right : (↑(↑u : Γ₀ˣ) : Γ₀) = (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v)
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) =
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
      ((embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
congr
-- Module: Mathlib.RingTheory.Valuation.Basic
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 →*₀ Γ₀))
right :
  (↑(↑u : Γ₀ˣ) : Γ₀) =
    (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑(WithZero.unzero ⋯) : WithZero ↥(valueGroup v))
⊢ (↑(↑u : Γ₀ˣ) : Γ₀) = (embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀) (↑γ : ValueGroup₀ v)

Tactic:
rw [← WithZero.coe_unzero (Units.ne_zero γ)]

Premises used: Units.ne_zero, WithZero.coe_unzero
-- Module: Mathlib.RingTheory.Valuation.Basic
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 →*₀ Γ₀)) → Γ₀) (↑(WithZero.unzero ⋯) : WithZero ↥(valueGroup v))

Tactic:
Eq.refl ..

Premises used: Eq.refl, WithZero.recZeroCoe
-- Module: Mathlib.RingTheory.Valuation.Basic
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 →*₀ Γ₀)) → Γ₀) (↑(WithZero.unzero ⋯) : WithZero ↥(valueGroup v))

Tactic:
exact Eq.refl ..

Premises used: Eq.refl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
Γ₀' : Type u_7
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
w : Valuation R Γ₀'
h :
  ∀ (r s : R),
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ↔
      LE.le.{u_7} (α := Γ₀') ((w : (a : R) → Γ₀') r : Γ₀') ((w : (a : R) → Γ₀') s : Γ₀')
⊢ ∀ (r s : R),
    LE.le.{u_4} (α := 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 →*₀ Γ₀)) ↔
      LE.le.{u_7} (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑w : R →*₀ Γ₀'))
        ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ₀')) r : ValueGroup₀ (F := R →*₀ Γ₀') (↑w : R →*₀ Γ₀'))
        ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ₀')) s : ValueGroup₀ (F := R →*₀ Γ₀') (↑w : R →*₀ Γ₀'))

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
γ : Γ₀ˣ
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
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) < (↑γ : Γ₀)
rwa₁ rwa₂ rwa₃ rwa₄ : (v : (a : R) → Γ₀) x_1 < (↑γ : Γ₀)
⊢ Membership.mem (γ := Set R) {x : R | (v : (a : R) → Γ₀) x < (↑γ : Γ₀)} (-x_1)

Tactic:
rwa [Set.mem_setOf, map_neg]

Premises used: Set.mem_setOf, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
x : R
⊢ x ∈ v.ltAddSubgroup γ ↔ (v : (a : R) → Γ₀) x < (↑γ : Γ₀)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Monotone v.ltAddSubgroup

Tactic:
fun _ _ h _ ↦ (Units.val_le_val.mpr h).trans_lt'

Premises used: Iff.mpr, Set.Mem, Monotone, setOf, Units.val_le_val, LE.le.trans_lt'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ v.ltAddSubgroup γ ≤ v.leAddSubgroup (↑γ : Γ₀)

Tactic:
fun _ h ↦ h.le

Premises used: Set.Mem, setOf, LT.lt.le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst_1 : Field K
v : Valuation K Γ₀
h : ∀ (x : K), x ∈ v.leAddSubgroup 0 ↔ Membership.mem (γ := AddSubgroup K) ⊥ x
⊢ v.leAddSubgroup 0 = ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst_1 : Field K
v : Valuation K Γ₀
x : K
⊢ x ∈ v.leAddSubgroup 0 ↔ Membership.mem (γ := AddSubgroup K) ⊥ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
obtain :
  ∀ (x : R) (hx0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hx1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)), Nontrivial Γ₀
⊢ Nontrivial Γ₀

Tactic:
obtain ⟨x, hx0, hx1⟩ := hv.exists_val_nontrivial

Premises used: Valuation.IsNontrivial.exists_val_nontrivial
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
hx0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Nontrivial Γ₀

Tactic:
⟨v x, 1, hx1⟩

Premises used: Nontrivial.mk, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
hv : v.IsNontrivial
x : R
hx0 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hx1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Nontrivial Γ₀

Tactic:
exact ⟨v x, 1, hx1⟩
-- Module: Mathlib.RingTheory.Valuation.Basic
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
inr : ∀ (hx0 : x ≠ 0), False
⊢ False

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
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
hx : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (0 : Γ₀)
hx' : Ne.{u_4 + 1} (α := Γ₀) ((1 : (a : R) → Γ₀) 0 : Γ₀) (1 : Γ₀)
⊢ False

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: Valuation.one_apply_of_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
hx0 : x ≠ 0
⊢ False

Tactic:
simp_all [one_apply_of_ne_zero]

Premises used: Valuation.one_apply_of_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
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
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)
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueMonoid v)

Tactic:
obtain ⟨x, h0, h1⟩ := hv.exists_val_nontrivial

Premises used: Valuation.IsNontrivial.exists_val_nontrivial
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
rw : ∃ (x : Γ₀ˣ), Membership.mem (γ := Submonoid Γ₀ˣ) (MonoidWithZeroHom.valueMonoid v) x ∧ x ≠ 1
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueMonoid v)

Tactic:
rw [Submonoid.nontrivial_iff_exists_ne_one]

Premises used: Submonoid.nontrivial_iff_exists_ne_one
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
right : Ne.{u_7 + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : R) → Γ₀) x) h0 : Γ₀ˣ) (1 : Γ₀ˣ)
⊢ ∃ (x : Γ₀ˣ), Membership.mem (γ := Submonoid Γ₀ˣ) (MonoidWithZeroHom.valueMonoid v) x ∧ x ≠ 1

Tactic:
use (Units.mk0 (v x) h0), MonoidWithZeroHom.mem_valueMonoid v (Set.mem_range_self x)

Premises used: MonoidWithZeroHom.mem_valueMonoid, Units.mk0, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
⊢ Ne.{u_7 + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : R) → Γ₀) x) h0 : Γ₀ˣ) (1 : Γ₀ˣ)

Tactic:
simpa [Units.ext_iff] using h1

Premises used: Units.ext_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
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
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)
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueGroup v)

Tactic:
obtain ⟨x, h0, h1⟩ := hv.exists_val_nontrivial

Premises used: Valuation.IsNontrivial.exists_val_nontrivial
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
rw : ∃ (x : Γ₀ˣ), Membership.mem (γ := Subgroup Γ₀ˣ) (MonoidWithZeroHom.valueGroup v) x ∧ x ≠ 1
⊢ Nontrivial.{u_7} ↥(MonoidWithZeroHom.valueGroup v)

Tactic:
rw [Subgroup.nontrivial_iff_exists_ne_one]

Premises used: Subgroup.nontrivial_iff_exists_ne_one
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
right : Ne.{u_7 + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : R) → Γ₀) x) h0 : Γ₀ˣ) (1 : Γ₀ˣ)
⊢ ∃ (x : Γ₀ˣ), Membership.mem (γ := Subgroup Γ₀ˣ) (MonoidWithZeroHom.valueGroup v) x ∧ x ≠ 1

Tactic:
use (Units.mk0 (v x) h0), MonoidWithZeroHom.mem_valueGroup v (Set.mem_range_self x)

Premises used: MonoidWithZeroHom.mem_valueGroup, Units.mk0, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
K : Type u_7
inst_1 : DivisionRing K
w : Valuation K Γ₀
⊢ w.IsNontrivial ↔ ∃ (x : Kˣ), Ne.{u_4 + 1} (α := Γ₀) ((w : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)

Tactic:
⟨fun ⟨x, hx0, hx1⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 0, hx0⟩
    ⟨Units.mk0 x (w.ne_zero_iff.mp hx0), hx1⟩,
    fun ⟨x, hx⟩ ↦
    have : Nontrivial Γ₀ := ⟨w x, 1, hx⟩
    ⟨x, w.ne_zero_iff.mpr (Units.ne_zero x), hx⟩⟩

Premises used: Iff.mpr, Units.val, Exists, Units.ne_zero, Ne, Nontrivial.mk, Valuation.ne_zero_iff, Units.mk0, _private.0.Valuation.isNontrivial_iff_exists_unit.match_1, Valuation.IsNontrivial, And.intro, _private.0.Valuation.isNontrivial_iff_exists_unit.match_2, Iff.intro, Exists.intro, Iff.mp, OfNat.ofNat, Valuation.IsNontrivial.mk, DFunLike.coe