awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
⊢ Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
          (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b) h) ⋯) :
            WithZero ↥(valueGroup v))) :
      WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b) ⋯) ⋯) :
          WithZero ↥(valueGroup Valued.v)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
have pos : ∀ (hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀)),
  Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
          (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b) h) sorry) :
            WithZero ↥(valueGroup v))) :
      WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b) sorry) sorry) :
          WithZero ↥(valueGroup Valued.v)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
Tactic: by_cases hb : v b = 0
-- 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 : v.IsEquiv w
⊢ UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)
have refine : ContinuousAt (X := WithVal v) (Y := R) (⇑(equiv v) : (a : WithVal v) → R) 0
Tactic: refine uniformContinuous_of_continuousAt_zero _ ?_
-- 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 : v.IsEquiv w
⊢ ContinuousAt (X := WithVal v) (Y := R) (⇑(equiv v) : (a : WithVal v) → R) 0
have simp_rw : ∀ (ib : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ),
  ∃ (ia : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ),
    ∀ (x : WithVal v),
      Membership.mem (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) 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)}
          ((equiv v : (a : WithVal v) → 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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
⊢ ∃ (ia : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ),
    ∀ (x : WithVal v),
      Membership.mem (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
              (↑ia : ValueGroup₀ Valued.v)}
          x →
        Membership.mem (α := R) (γ := Set R)
          {x : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
              (↑γ : ValueGroup₀ Valued.v)}
          ((equiv v : (a : WithVal v) → R) x : R)
have obtain : ∀ (r s : R) (hr₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') r : Γ₀'))
  (hs₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') s : Γ₀'))
  (hr :
    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 :
          ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
        ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s :
          ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) =
      (↑γ : ValueGroup₀ Valued.v)),
  ∃ (ia : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ),
    ∀ (x : WithVal v),
      Membership.mem (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
              (↑ia : ValueGroup₀ Valued.v)}
          x →
        Membership.mem (α := R) (γ := Set R)
          {x : R |
            (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x <
              (↑γ : ValueGroup₀ Valued.v)}
          ((equiv v : (a : WithVal v) → R) x : R)
Tactic: obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ
-- 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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
r s : R
hr₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') r : Γ₀')
hs₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') s : Γ₀')
hr :
  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 :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) =
    (↑γ : ValueGroup₀ Valued.v)
x : WithVal v
hx :
  Membership.mem (γ := Set (WithVal v))
    {x : WithVal v |
      (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
        (↑(Units.mk0
              (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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → 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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → WithVal v) s) :
                  ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)))
              ⋯) :
          ValueGroup₀ Valued.v)}
    x
y : R := (equiv v : (a : WithVal v) → R) x
⊢ Membership.mem (α := R) (γ := Set R)
    {x : R |
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x < (↑γ : ValueGroup₀ Valued.v)}
    ((equiv v : (a : WithVal v) → R) x : R)
have hy : toVal v y = x
Tactic: have hy : toVal v y = x := rfl
-- 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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
r s : R
hr₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') r : Γ₀')
hs₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') s : Γ₀')
hr :
  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 :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) =
    (↑γ : ValueGroup₀ Valued.v)
x : WithVal v
hx :
  Membership.mem (γ := Set (WithVal v))
    {x : WithVal v |
      (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
        (↑(Units.mk0
              (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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → 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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → WithVal v) s) :
                  ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)))
              ⋯) :
          ValueGroup₀ Valued.v)}
    x
y : R := (equiv v : (a : WithVal v) → R) x
hy : toVal v y = x
⊢ Membership.mem (α := R) (γ := Set R)
    {x : R |
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x < (↑γ : ValueGroup₀ Valued.v)}
    ((equiv v : (a : WithVal v) → R) x : R)
have hs0' : LT.lt.{u_5} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
  (0 : 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 →*₀ Γ₀)) (toVal v s) :
    ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
Tactic: have hs0' : 0 < Valued.v.restrict (toVal v s) := by
    simp [restrict_pos_iff, h.pos_iff, ← hv, hs₀]
-- 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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
r s : R
hr₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') r : Γ₀')
hs₀ : LT.lt.{u_6} (α := Γ₀') (0 : Γ₀') ((Valued.v : (a : R) → Γ₀') s : Γ₀')
hr :
  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 :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀'))
      ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) s :
        ValueGroup₀ (F := R →*₀ Γ₀') (↑Valued.v : R →*₀ Γ₀')) =
    (↑γ : ValueGroup₀ Valued.v)
x : WithVal v
hx :
  Membership.mem (γ := Set (WithVal v))
    {x : WithVal v |
      (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
        (↑(Units.mk0
              (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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → 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 →*₀ Γ₀))
                    (((equiv v).symm : (a : R) → WithVal v) s) :
                  ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)))
              ⋯) :
          ValueGroup₀ Valued.v)}
    x
y : R := (equiv v : (a : WithVal v) → R) x
hy : toVal v y = x
hs0' :
  LT.lt.{u_5} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
    (0 : 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 →*₀ Γ₀)) (toVal v s) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
⊢ Membership.mem (α := R) (γ := Set R)
    {x : R |
      (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x < (↑γ : ValueGroup₀ Valued.v)}
    ((equiv v : (a : WithVal v) → R) x : R)
have h' : v.restrict.IsEquiv w.restrict
Tactic: have h' : v.restrict.IsEquiv w.restrict := h.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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ UniformContinuous (α := R) (β := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v)
have refine : ContinuousAt (X := R) (Y := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v) 0
Tactic: refine uniformContinuous_of_continuousAt_zero _ ?_
-- 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
⊢ ContinuousAt (X := R) (Y := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v) 0
have simp_rw : ∀ (ib : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) 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 (α := WithVal v) (γ := Set (WithVal v))
          {x : WithVal v |
            (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) x <
              (↑ib : ValueGroup₀ Valued.v)}
          (((equiv v).symm : (a : R) → WithVal v) x : WithVal v)
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 Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) 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 (α := 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 obtain : ∀ (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)),
  ∃ (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 (α := 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)
Tactic: obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ
-- 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 Γ₀'
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)
⊢ ∃ (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 (α := 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' : w.restrict.IsEquiv v.restrict
Tactic: have h' : w.restrict.IsEquiv v.restrict := h.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 Γ₀'
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
⊢ 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 →*₀ Γ₀')) ≠
    0
have simp : ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r.ofVal : Γ₀) (0 : Γ₀) ∧
  ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) (0 : Γ₀)
Tactic: simp only [equiv_apply, restrict_def, restrict₀_eq_zero_iff, ne_eq, div_eq_zero_iff, not_or,
      hv, (eq_zero h (r := r.ofVal)).ne, (eq_zero h (r := s.ofVal)).ne]