awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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 :
  Membership.mem (γ := Set R)
    {x : R |
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
        (↑(Units.mk0
              (HDiv.hDiv (α := ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) (β :=
                ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
                ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀'))
                    ((equiv v : (a : WithVal v) → R) r) :
                  ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
                ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀'))
                    ((equiv v : (a : WithVal v) → R) s) :
                  ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')))
              ⋯) :
          ValueGroup₀ Valued.v)}
    x
⊢ Membership.mem (α := WithVal v) (γ := Set (WithVal v))
    {x : WithVal v |
      (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
        (↑γ : ValueGroup₀ Valued.v)}
    (((equiv v).symm : (a : R) → WithVal v) x : WithVal v)
have h₁ : (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
  (↑γ : ValueGroup₀ Valued.v)
Tactic: simp only [equiv_symm_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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 →*₀ Γ₀'))
⊢ (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)
have 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)
Tactic: rw [lt_div_iff₀, ← map_mul, restrict_lt_iff, hv, h.lt_iff_lt, map_mul] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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)
⊢ (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)
have 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 →*₀ Γ₀'))
Tactic: rw [lt_div_iff₀, ← map_mul, restrict_lt_iff, hv, h.lt_iff_lt, map_mul] at hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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
⊢ (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)
have 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)
Tactic: rw [← hr, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), ← map_mul, ← lt_def,
      ← h.orderRingIso_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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
⊢ 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)
have h₁ : LT.lt.{u_5} (α := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x * s) : Γ₀)
  ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
Tactic: simp only [orderRingIso_apply, toVal_mul, lt_def, ofVal_mul, restrict_lt_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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
⊢ LT.lt.{u_5} (α := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x * s) : Γ₀)
    ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
have h₁ : HMul.hMul (α := Γ₀) (β := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v x) : Γ₀)
    ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀) <
  (Valued.v : (a : WithVal v) → Γ₀) r
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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_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 →*₀ Γ₀'))
have h₁ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀)
Tactic: rw [restrict_pos_iff, hv, h.pos_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (hypothesis)
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
⊢ UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
have h_val : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (hypothesis)
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
⊢ UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
have h_res : v.restrict.IsEquiv w.restrict
Tactic: have h_res : v.restrict.IsEquiv w.restrict := h_val.restrict
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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)
have refine : ContinuousAt (X := R) (Y := R) (⇑(RingHom.id R) : (a : R) → R) 0
Tactic: refine @uniformContinuous_of_continuousAt_zero _ _ (Valued.mk' w).toUniformSpace _ _
    _ (Valued.mk' v).toUniformSpace _ _ _ _ (RingHom.id R) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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
⊢ ContinuousAt (X := R) (Y := R) (⇑(RingHom.id R) : (a : R) → R) 0
have 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)
Tactic: simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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 ⋯
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨a, ha, y, hu⟩ := (mem_valueGroup_iff_of_comm _).mp u.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
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 ⋯
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)
have simp : ∃ (ia : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
  ∀ (x_1 : R),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x_1 < (↑ia : ValueGroup₀ Valued.v) →
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x_1 < (↑x : ValueGroup₀ Valued.v)
Tactic: simp only [Set.mem_setOf_eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (hypothesis)
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 ⋯
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),
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x_1 < (↑ia : ValueGroup₀ Valued.v) →
        (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x_1 < (↑x : ValueGroup₀ Valued.v)
have hy₀_def : let y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v);
y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
Tactic: set y₀ := h_val.orderMonoidIso x with hy₀_def