awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
    HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) r.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
h₁ :
  ∀
    (hx :
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
        (v : (a : R) → Γ₀) r.ofVal),
    (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
      (↑γ : ValueGroup₀ Valued.v)
h₂ :
  LT.lt.{u_6} (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
    ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
⊢ (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)

Tactic:
rw [lt_div_iff₀, ← map_mul, restrict_lt_iff, hv, h.lt_iff_lt, map_mul] at hx

Premises used: lt_div_iff₀, Valuation.IsEquiv.lt_iff_lt, map_mul, Valuation.restrict_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
    (v : (a : R) → Γ₀) r.ofVal
h₁ :
  LT.lt (α :=
    WithVal (R := WithVal v) (Γ₀ :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      (Valuation.restrict Valued.v))
    (toVal (Valuation.restrict Valued.v)
      (HMul.hMul (α := WithVal v) ((h.orderRingIso : (a : WithVal w) → WithVal v) (toVal w x) : WithVal v) s))
    (toVal (Valuation.restrict Valued.v) r)
⊢ (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)

Tactic:
rw [← hr, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), ← map_mul, ← lt_def,
      ← h.orderRingIso_apply]

Premises used: Iff.mpr, Valuation.IsEquiv.orderRingIso_apply, lt_div_iff₀, Valued.v, WithVal.lt_def, Valuation.restrict_pos_iff, map_mul
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
    (v : (a : R) → Γ₀) r.ofVal
h₁ :
  LT.lt.{u_5} (α := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x * s) : Γ₀)
    ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
⊢ LT.lt (α :=
    WithVal (R := WithVal v) (Γ₀ :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      (Valuation.restrict Valued.v))
    (toVal (Valuation.restrict Valued.v)
      (HMul.hMul (α := WithVal v) ((h.orderRingIso : (a : WithVal w) → WithVal v) (toVal w x) : WithVal v) s))
    (toVal (Valuation.restrict Valued.v) r)

Tactic:
simp only [orderRingIso_apply, toVal_mul, lt_def, ofVal_mul, restrict_lt_iff]

Premises used: Valuation.IsEquiv.orderRingIso_apply, WithVal.ofVal_mul, WithVal.toVal_mul, WithVal.lt_def, Valuation.restrict_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
    (v : (a : R) → Γ₀) r.ofVal
h₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x) : Γ₀)
      ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀) <
    (Valued.v : (a : WithVal v) → Γ₀) r
⊢ LT.lt.{u_5} (α := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x * s) : Γ₀)
    ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
    (v : (a : R) → Γ₀) r.ofVal
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x) : Γ₀)
      ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀) <
    (Valued.v : (a : WithVal v) → Γ₀) r

Tactic:
hx
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) <
    (v : (a : R) → Γ₀) r.ofVal
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x) : Γ₀)
      ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀) <
    (Valued.v : (a : WithVal v) → Γ₀) r

Tactic:
exact hx
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
    HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) r.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
h₁ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀)
⊢ LT.lt.{u_6} (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
    ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))

Tactic:
rw [restrict_pos_iff, hv, h.pos_iff]

Premises used: Valuation.IsEquiv.pos_iff, Valuation.restrict_pos_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
    HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) r.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
⊢ LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀)

Tactic:
hs₀
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
    HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
      ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) r.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s.ofVal :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
⊢ LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀)

Tactic:
exact hs₀
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
⊢ IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v

Tactic:
have h_val : ((Valued.mk' v).v).IsEquiv (Valued.mk' w).v := h
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
⊢ v.restrict.IsEquiv w.restrict

Tactic:
have h_res : v.restrict.IsEquiv w.restrict := h_val.restrict
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
h_res : v.restrict.IsEquiv w.restrict
⊢ UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)

Tactic:
@uniformContinuous_of_continuousAt_zero _ _ (Valued.mk' w).toUniformSpace _ _
    _ (Valued.mk' v).toUniformSpace _ _ _ _ (RingHom.id R) ?_

Premises used: uniformContinuous_of_continuousAt_zero, RingHom.id
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
h_res : v.restrict.IsEquiv w.restrict
refine : ContinuousAt (X := R) (Y := R) (⇑(RingHom.id R) : (a : R) → R) 0
⊢ UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)

Tactic:
refine @uniformContinuous_of_continuousAt_zero _ _ (Valued.mk' w).toUniformSpace _ _
    _ (Valued.mk' v).toUniformSpace _ _ _ _ (RingHom.id R) ?_

Premises used: uniformContinuous_of_continuousAt_zero, RingHom.id
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
h_res : v.restrict.IsEquiv w.restrict
simp_rw :
  ∀ (ib : (ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ),
    ∃ (ia : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
      ∀ (x : R),
        Membership.mem (γ := Set R)
            {x : R |
              (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
                (↑ia : ValueGroup₀ Valued.v)}
            x →
          Membership.mem (α := R) (γ := Set R)
            {x : R |
              (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x <
                (↑ib : ValueGroup₀ Valued.v)}
            ((RingHom.id R : (a : R) → R) x : R)
⊢ ContinuousAt (X := R) (Y := R) (⇑(RingHom.id R) : (a : R) → R) 0

Tactic:
simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, Valued.hasBasis_nhds_zero, map_zero, forall_const, true_and
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : IsEquiv.{u_4, u_5, u_6} (R := R) Valued.v Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
u : ↥(valueGroup (F := Valuation R Γ₀) Valued.v) := WithZero.unzero ⋯
obtain :
  ∀ (a : R) (ha : Ne.{u_5 + 1} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (0 : Γ₀)) (y : R)
    (hu : HMul.hMul (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (Valued.v : (a : R) → Γ₀) y),
    ∃ (ia : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
      ∀ (x_1 : R),
        Membership.mem (γ := Set R)
            {x : R |
              (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
                (↑ia : ValueGroup₀ Valued.v)}
            x_1 →
          Membership.mem (α := R) (γ := Set R)
            {x_2 : R |
              (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x_2 <
                (↑x : ValueGroup₀ Valued.v)}
            ((RingHom.id R : (a : R) → R) x_1 : R)
⊢ ∃ (ia : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
    ∀ (x_1 : R),
      Membership.mem (γ := Set R)
          {x : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
              (↑ia : ValueGroup₀ Valued.v)}
          x_1 →
        Membership.mem (α := R) (γ := Set R)
          {x_2 : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x_2 <
              (↑x : ValueGroup₀ Valued.v)}
          ((RingHom.id R : (a : R) → R) x_1 : R)

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

Premises used: Iff.mp, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, Subtype.property