awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ'₀
⊢ (∀ (r s : R),
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) s : Γ'₀) ((v' : (a : R) → Γ'₀) r : Γ'₀)) ↔
    ∀ {x y : R},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)

Tactic:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ'₀
⊢ (∀ (r s : R),
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) s : Γ'₀) ((v' : (a : R) → Γ'₀) r : Γ'₀)) ↔
    ∀ {x y : R},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.RingTheory.Valuation.Basic
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'
hv : v.IsNontrivial
obtain :
  ∀ (x : R)
    (hx :
      Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
        Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)),
    v'.IsNontrivial
⊢ v'.IsNontrivial

Tactic:
obtain ⟨x, hx⟩ := hv
-- Module: Mathlib.RingTheory.Valuation.Basic
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'
x : R
hx :
  Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ :
  Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀) ∧
    Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v'.IsNontrivial

Tactic:
use x
-- Module: Mathlib.RingTheory.Valuation.Basic
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'
x : R
hx :
  Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀) ∧
    Ne.{u_5 + 1} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
simpa [← Valuation.IsEquiv.eq_one_iff_eq_one h, ← Valuation.IsEquiv.eq_zero h]

Premises used: Valuation.IsEquiv.eq_zero, Valuation.IsEquiv.eq_one_iff_eq_one
-- Module: Mathlib.RingTheory.Valuation.Basic
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'
⊢ v.IsNontrivial ↔ v'.IsNontrivial

Tactic:
⟨fun hv ↦ isNontrivial_of_isEquiv h hv, fun hv ↦ isNontrivial_of_isEquiv h.symm hv⟩

Premises used: Iff.intro, Valuation.IsEquiv.symm, Valuation.isNontrivial_of_isEquiv
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hs : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀)
⊢ ¬Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀)
hs : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀)
rw :
  Eq (α := ValueGroup₀ w)
    (have c :=
      ⋯.choose (p :=
        fun
          (d :
            { xy : R × R //
              Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
        Eq (α := ValueGroup₀ v) (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v))
          (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)));
    (↑(valueGroup.mk w (↑c : R × R).1 (↑c : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup w)))
    (↑(valueGroup.mk w r s ⋯ ⋯) : WithZero ↥(valueGroup w))
⊢ h.valueGroup₀Fun (↑(valueGroup.mk v r s hr hs) : WithZero ↥(valueGroup v)) =
    (↑(valueGroup.mk w r s ⋯ ⋯) : WithZero ↥(valueGroup w))

Tactic:
rw [valueGroup₀Fun, dif_neg (by simp)]

Premises used: Valuation.IsEquiv.valueGroup₀Fun, dif_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
⊢ h.valueGroup₀Fun 0 = 0

Tactic:
simp [valueGroup₀Fun]

Premises used: Valuation.IsEquiv.valueGroup₀Fun
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ v
inl : x = 0 → ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x
inr :
  ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀))
    (hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)),
    ⋯.valueGroup₀Fun (h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))) =
      (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x

Tactic:
obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ v
h_1 : x = 0
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun x) = x

Tactic:
simp_all [valueGroup₀Fun_zero]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_zero
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀)
hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)
⊢ ⋯.valueGroup₀Fun (h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))) =
    (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))

Tactic:
simp [valueGroup₀Fun_spec]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_spec
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ w
inl : x = 0 → h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x
inr :
  ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) r₁ : Γ'₀) (0 : Γ'₀))
    (hs₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) s₁ : Γ'₀) (0 : Γ'₀)),
    h.valueGroup₀Fun (⋯.valueGroup₀Fun (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))) =
      (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x

Tactic:
obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x : ValueGroup₀ w
h_1 : x = 0
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun x) = x

Tactic:
simp_all [valueGroup₀Fun_zero]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_zero
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) r₁ : Γ'₀) (0 : Γ'₀)
hs₁ : Ne.{u_5 + 1} (α := Γ'₀) ((w : (a : R) → Γ'₀) s₁ : Γ'₀) (0 : Γ'₀)
⊢ h.valueGroup₀Fun (⋯.valueGroup₀Fun (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))) =
    (↑(valueGroup.mk w r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup w))

Tactic:
simp [valueGroup₀Fun_spec]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_spec
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
inl : x = 0 → h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y
inr :
  ∀ (r₁ s₁ : R) (hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀))
    (hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)),
    h.valueGroup₀Fun ((↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * y) =
      h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * h.valueGroup₀Fun y
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y

Tactic:
obtain _ | ⟨r₁, s₁, hr₁, hs₁, rfl⟩ := x.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
h_1 : x = 0
⊢ h.valueGroup₀Fun (x * y) = h.valueGroup₀Fun x * h.valueGroup₀Fun y

Tactic:
simp_all [valueGroup₀Fun_zero]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_zero
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
y : ValueGroup₀ v
r₁ s₁ : R
hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀)
hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)
inr :
  y = 0 →
    h.valueGroup₀Fun ((↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * y) =
      h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * h.valueGroup₀Fun y
inr₁ :
  ∀ (r₂ s₂ : R) (hr₂ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₂ : Γ₀) (0 : Γ₀))
    (hs₂ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₂ : Γ₀) (0 : Γ₀)),
    h.valueGroup₀Fun
        (HMul.hMul (α := ValueGroup₀ v) (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))
          (↑(valueGroup.mk v r₂ s₂ hr₂ hs₂) : WithZero ↥(valueGroup v))) =
      h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) *
        h.valueGroup₀Fun (↑(valueGroup.mk v r₂ s₂ hr₂ hs₂) : WithZero ↥(valueGroup v))
⊢ h.valueGroup₀Fun ((↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * y) =
    h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * h.valueGroup₀Fun y

Tactic:
obtain _ | ⟨r₂, s₂, hr₂, hs₂, rfl⟩ := y.zero_or_exists_mk

Premises used: MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk, rfl
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
y : ValueGroup₀ v
r₁ s₁ : R
hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀)
hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)
h_1 : y = 0
⊢ h.valueGroup₀Fun ((↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * y) =
    h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) * h.valueGroup₀Fun y

Tactic:
simp_all [valueGroup₀Fun_zero]

Premises used: Valuation.IsEquiv.valueGroup₀Fun_zero
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
r₁ s₁ : R
hr₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₁ : Γ₀) (0 : Γ₀)
hs₁ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₁ : Γ₀) (0 : Γ₀)
r₂ s₂ : R
hr₂ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r₂ : Γ₀) (0 : Γ₀)
hs₂ : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s₂ : Γ₀) (0 : Γ₀)
⊢ h.valueGroup₀Fun
      (HMul.hMul (α := ValueGroup₀ v) (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v))
        (↑(valueGroup.mk v r₂ s₂ hr₂ hs₂) : WithZero ↥(valueGroup v))) =
    h.valueGroup₀Fun (↑(valueGroup.mk v r₁ s₁ hr₁ hs₁) : WithZero ↥(valueGroup v)) *
      h.valueGroup₀Fun (↑(valueGroup.mk v r₂ s₂ hr₂ hs₂) : WithZero ↥(valueGroup v))

Tactic:
simp [← WithZero.coe_mul, valueGroup.mk_mul, valueGroup₀Fun_spec]

Premises used: MonoidWithZeroHom.valueGroup.mk_mul, Valuation.IsEquiv.valueGroup₀Fun_spec, WithZero.coe_mul
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
simp :
  LE.le.{u_5} (α := ValueGroup₀ w)
      (if h : x = 0 then 0
      else
        (↑(valueGroup.mk w
              (↑(⋯.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                  R × R).1
              (↑(⋯.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                  R × R).2
              ⋯ ⋯) :
          WithZero ↥(valueGroup w)))
      (if h : y = 0 then 0
      else
        (↑(valueGroup.mk w
              (↑(⋯.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                  R × R).1
              (↑(⋯.choose (p :=
                      fun
                        (d :
                          { xy : R × R //
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                              ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                      y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                  R × R).2
              ⋯ ⋯) :
          WithZero ↥(valueGroup w))) ↔
    x ≤ y
⊢ h.valueGroup₀Fun x ≤ h.valueGroup₀Fun y ↔ x ≤ y

Tactic:
simp only [valueGroup₀Fun, ne_eq]

Premises used: Valuation.IsEquiv.valueGroup₀Fun, ne_eq
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
hx0 : x = 0
hy0 : y = 0
⊢ LE.le.{u_5} (α := ValueGroup₀ w) 0 0 ↔ x ≤ y

Tactic:
simp [hx0, hy0]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
hx0 : x = 0
hy0 : ¬y = 0
⊢ LE.le (α := ValueGroup₀ w) 0
      (↑(valueGroup.mk w
            (↑(⋯.choose (p :=
                    fun
                      (d :
                        { xy : R × R //
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(⋯.choose (p :=
                    fun
                      (d :
                        { xy : R × R //
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                    y = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).2
            ⋯ ⋯) :
        WithZero ↥(valueGroup w)) ↔
    x ≤ y

Tactic:
simp [hx0]
-- 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 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
inst_3 : LinearOrderedCommGroupWithZero Γ''₀
inst_4 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : ValueGroup₀ v
hx0 : ¬x = 0
hy0 : y = 0
⊢ LE.le (α := ValueGroup₀ w)
      (↑(valueGroup.mk w
            (↑(⋯.choose (p :=
                    fun
                      (d :
                        { xy : R × R //
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(⋯.choose (p :=
                    fun
                      (d :
                        { xy : R × R //
                          ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.1 : Γ₀) (0 : Γ₀) ∧
                            ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) xy.2 : Γ₀) (0 : Γ₀) }) ↦
                    x = (↑(valueGroup.mk v (↑d : R × R).1 (↑d : R × R).2 ⋯ ⋯) : WithZero ↥(valueGroup v)))) :
                R × R).2
            ⋯ ⋯) :
        WithZero ↥(valueGroup w))
      0 ↔
    x ≤ y

Tactic:
simp [hx0, hy0]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
⊢ v.restrict.IsEquiv w.restrict

Tactic:
have h_res := h.restrict
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
pos :
  ∀ (ha : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)),
    Eq.{u_5 + 1} (α := ValueGroup₀ w)
      ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a) :
        ValueGroup₀ w)
      ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
neg :
  ∀ (ha : ¬Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)),
    Eq.{u_5 + 1} (α := ValueGroup₀ w)
      ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a) :
        ValueGroup₀ w)
      ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
⊢ Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))

Tactic:
by_cases ha : v a = 0

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ'₀
inst_2 : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
a : R
h_res : v.restrict.IsEquiv w.restrict
ha : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)

Tactic:
rw [← restrict₀_eq_zero_iff] at ha

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff