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 Γ₀
x y : R
pos :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
neg :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
pos₁ :
  ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) →
      (LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          (0 : ValueGroup₀ v) ↔
        LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
neg₁ :
  ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
split_ifs with hx hy
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [zero_lt_iff.mpr, ← Units.val_lt_val]

Premises used: Iff.mpr, zero_lt_iff, Units.val_lt_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [zero_lt_iff.mpr, ← Units.val_lt_val]

Premises used: Iff.mpr, zero_lt_iff, Units.val_lt_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      (0 : ValueGroup₀ v) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [zero_lt_iff.mpr, ← Units.val_lt_val]

Premises used: Iff.mpr, zero_lt_iff, Units.val_lt_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [zero_lt_iff.mpr, ← Units.val_lt_val]

Premises used: Iff.mpr, zero_lt_iff, Units.val_lt_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
    LE.le.{u_4} (α := 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 →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
aesop (add norm [restrict_def, restrict₀_apply])

Premises used: Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
rw :
  LT.lt (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
| LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
rw [← ValueGroup₀.embedding_restrict₀ x]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
conv_rhs :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    LT.lt (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
conv_rhs => rw [← ValueGroup₀.embedding_restrict₀ x]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
rw :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g
rw₁ rw₂ :
  ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x < g
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < g ↔
    LT.lt (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
rw [embedding_strictMono.lt_iff_lt, restrict_def]

Premises used: StrictMono.lt_iff_lt, 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 Γ₀
x : R
g : ValueGroup₀ v
rw :
  LE.le (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
| LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
rw [← ValueGroup₀.embedding_restrict₀ x]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
conv_rhs :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
conv_rhs => rw [← ValueGroup₀.embedding_restrict₀ x]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : ValueGroup₀ v
rw :
  (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g
rw₁ rw₂ :
  ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g ↔
    ((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x ≤ g
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ g ↔
    LE.le (α := Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x :
            ValueGroup₀ v) :
        Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) g : Γ₀)

Tactic:
rw [embedding_strictMono.le_iff_le, restrict_def]

Premises used: Valuation.restrict_def, StrictMono.le_iff_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
rw₁ rw₂ :
  LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [restrict_lt_iff_lt_embedding, map_one]

Premises used: Valuation.restrict_lt_iff_lt_embedding, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
rw₁ rw₂ :
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [restrict_le_iff_le_embedding, map_one]

Premises used: Valuation.restrict_le_iff_le_embedding, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
rw :
  Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 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 →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
rw [restrict_def, restrict₀_eq_zero_iff]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_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 Γ₀
x : R
rw :
  Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
      (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{u_4 + 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 →*₀ Γ₀)) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [restrict_def, restrict₀_eq_one_iff]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_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 Γ₀
x y : R
pos :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
neg :
  ∀ (hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
pos₁ :
  ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) →
      (LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
              WithZero ↥(valueGroup v)) :
            WithZero ↥(valueGroup v))
          (0 : ValueGroup₀ v) ↔
        LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀))
neg₁ :
  ∀ (hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
    (h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
    LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v))
        ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
            WithZero ↥(valueGroup v)) :
          WithZero ↥(valueGroup v)) ↔
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
split_ifs with hx hy
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) 0 0 ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
hy : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ v)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) hy) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      (0 : ValueGroup₀ v) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) hx) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v))
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup v)) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
simp_all [← Units.val_le_val]

Premises used: Units.val_le_val
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) x) h) ⋯) :
          WithZero ↥(valueGroup v)))
      (if h : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) y) h) ⋯) :
          WithZero ↥(valueGroup v))) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ (↑v : R →*₀ Γ₀)) → Γ₀)
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) :
      Γ₀)
    ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
embedding_restrict₀ x

Premises used: Set.Mem, setOf, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ValueGroup₀ v)ˣ
⊢ let u := WithZero.unzero ⋯;
  u = WithZero.unzero ⋯

Tactic:
set u := WithZero.unzero (Units.ne_zero γ) with hu_def

Premises used: Units.ne_zero, WithZero.unzero