awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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.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
have 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
Tactic: obtain _ | ⟨r₂, s₂, hr₂, hs₂, rfl⟩ := y.zero_or_exists_mk
-- 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 : 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
⊢ 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
have 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))
Tactic: obtain _ | ⟨r₂, s₂, hr₂, hs₂, rfl⟩ := y.zero_or_exists_mk
Cleared hypotheses: y
-- 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 : 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.valueGroup₀Fun x ≤ h.valueGroup₀Fun y ↔ x ≤ y
have simp : LE.le.{u_5} (α := ValueGroup₀ w)
    (if h : x = 0 then 0
    else
      (↑(valueGroup.mk w
            (↑(sorry.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 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(sorry.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 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).2
            sorry sorry) :
        WithZero ↥(valueGroup w)))
    (if h : y = 0 then 0
    else
      (↑(valueGroup.mk w
            (↑(sorry.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 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).1
            (↑(sorry.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 sorry sorry) : WithZero ↥(valueGroup v)))) :
                R × R).2
            sorry sorry) :
        WithZero ↥(valueGroup w))) ↔
  x ≤ y
Tactic: simp only [valueGroup₀Fun, ne_eq]
-- 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 : 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
⊢ 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
have pos : ∀ (hx0 : x = 0) (hy0 : y = 0), LE.le.{u_5} (α := ValueGroup₀ w) 0 0 ↔ x ≤ y
Tactic: split_ifs with hx0 hy0 hy0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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
⊢ 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 →*₀ Γ'₀))
have h_res : v.restrict.IsEquiv w.restrict
Tactic: have h_res := h.restrict
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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
⊢ 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 →*₀ Γ'₀))
have 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 →*₀ Γ'₀))
Tactic: by_cases ha : v a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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 →*₀ Γ'₀))
⊢ 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 →*₀ Γ'₀))
have 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 →*₀ Γ'₀))
Tactic: by_cases ha : v a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
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_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 →*₀ Γ'₀))
have ha₁ : 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
⊢ 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 →*₀ Γ'₀))
have pos : Eq.{u_5 + 1} (α := ValueGroup₀ w)
  ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
      (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a) :
    ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
Tactic: rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
pos :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) 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 →*₀ Γ'₀))
have pos₁ : Eq.{u_5 + 1} (α := ValueGroup₀ w) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) 0 : ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
Tactic: rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
pos :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₁ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) 0 : 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 →*₀ Γ'₀))
have pos₂ : Eq.{u_5 + 1} (α := ValueGroup₀ w) (0 : ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
Tactic: rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
pos :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₁ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) 0 : ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₂ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) (0 : 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 →*₀ Γ'₀))
have pos₃ : Eq.{u_5 + 1} (α := ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
  (0 : ValueGroup₀ w)
Tactic: rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
pos :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w)
        (((restrict₀ v : MonoidWithZeroHom.{u_3, u_4} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₁ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) 0 : ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₂ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w) (0 : ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
pos₃ :
  Eq.{u_5 + 1} (α := ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
    (0 : ValueGroup₀ w)
⊢ 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 →*₀ Γ'₀))
have pos₄ : Eq.{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: rwa [restrict_def, ha, map_zero, Eq.comm, ← h_res.eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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_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 →*₀ Γ'₀))
have neg : Eq.{u_5 + 1} (α := ValueGroup₀ w)
  ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) (↑(valueGroup.mk v 1 a sorry ha) : WithZero ↥(valueGroup v)) :
    ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
Tactic: rw [(v.restrict_eq_mk ha)]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
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_5 + 1} (α := ValueGroup₀ w)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ w) (↑(valueGroup.mk v 1 a ⋯ ha) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ w)
    ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
have h₁ : Eq.{u_5 + 1} (α := ValueGroup₀ w)
  ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ'₀)) a : ValueGroup₀ (F := R →*₀ Γ'₀) (↑w : R →*₀ Γ'₀))
  ((↑(valueGroup.mk w 1 a sorry sorry) : WithZero ↥(valueGroup w)) : WithZero ↥(valueGroup w))
Tactic: convert! valueGroup₀Fun_spec (h := h) (hs := ha) (r := 1) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
⊢ h.orderMonoidIso = OrderMonoidIso.refl (ValueGroup₀ v)
have h₁ : ∀ (x : ValueGroup₀ v),
  Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x : ValueGroup₀ v
⊢ Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
have h₁ : Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
  ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
Tactic: obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x : ValueGroup₀ v
h₁ :
  Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) 0 : ValueGroup₀ v)
⊢ Eq (α := ValueGroup₀ v) ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v) x : ValueGroup₀ v)
have h₂ : ∀ (x y : R) (w : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀))
  (w_1 : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)),
  Eq (α := ValueGroup₀ v)
    ((h.orderMonoidIso : (a : ValueGroup₀ v) → ValueGroup₀ v)
        (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
    ((OrderMonoidIso.refl (ValueGroup₀ v) : (a : ValueGroup₀ v) → ValueGroup₀ v)
        (↑(valueGroup.mk v x y w w_1) : WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
Tactic: obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
Cleared hypotheses: x