awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
⊢ ∃ (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₀_ne_zero : y₀ ≠ 0
Tactic: have hy₀_ne_zero : y₀ ≠ 0 := by simp [hy₀_def]
-- 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
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_ne_zero : y₀ ≠ 0
⊢ ∃ (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 := Units.mk0 y₀ hy₀_ne_zero;
y = Units.mk0 y₀ hy₀_ne_zero
Tactic: set y := (Units.mk0 y₀ hy₀_ne_zero) with hy_def
-- 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_1 : R
hu : HMul.hMul (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (Valued.v : (a : R) → Γ₀) y_1
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_ne_zero : y₀ ≠ 0
y : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
⊢ ∃ (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 h₁ : ∀ (x_1 : R),
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) x_1 < (↑y : ValueGroup₀ Valued.v) →
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x_1 < (↑x : ValueGroup₀ Valued.v)
Tactic: use y
-- 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_1 : R
hu : HMul.hMul (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (Valued.v : (a : R) → Γ₀) y_1
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_ne_zero : y₀ ≠ 0
y : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) b < (↑y : ValueGroup₀ Valued.v)
⊢ (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
have h₁ : ∀
  (hb :
    (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
        ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
      (↑y : ValueGroup₀ Valued.v)),
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
Tactic: rwa [← h_val.orderMonoidIso_spec, hy_def, Units.val_mk0, hy₀_def,
    h_val.orderMonoidIso.strictMono.lt_iff_lt] at hb
Cleared hypotheses: hb
-- 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_1 : R
hu : HMul.hMul (α := Γ₀) ((Valued.v : (a : R) → Γ₀) a : Γ₀) (↑(↑u : Γ₀ˣ) : Γ₀) = (Valued.v : (a : R) → Γ₀) y_1
y₀ : ValueGroup₀ (F := Valuation R Γ₀') Valued.v :=
  (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_def : y₀ = (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v) (↑x : ValueGroup₀ Valued.v)
hy₀_ne_zero : y₀ ≠ 0
y : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
hb : (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀')) b < (↑y : ValueGroup₀ Valued.v)
h₁ :
  ∀
    (hb :
      (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
          ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
        (↑y : ValueGroup₀ Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
h₂ :
  ∀
    (hb :
      (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
          ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
        (↑(Units.mk0 y₀ hy₀_ne_zero) : ValueGroup₀ Valued.v)),
    (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
⊢ (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
have h₃ : ∀
  (hb :
    (h_val.orderMonoidIso : (a : ValueGroup₀ Valued.v) → ValueGroup₀ Valued.v)
        ((Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b) <
      y₀),
  (Valuation.restrict Valued.v : (a : R) → ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) b < (↑x : ValueGroup₀ Valued.v)
Tactic: rwa [← h_val.orderMonoidIso_spec, hy_def, Units.val_mk0, hy₀_def,
    h_val.orderMonoidIso.strictMono.lt_iff_lt] at hb
Cleared hypotheses: hb
-- 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 (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → WithVal w)
have hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
Tactic: have hcomp : WithVal.congr v w (.refl R) = _ := RingEquiv.ext_iff.mpr (congrFun 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 Γ₀'
h : v.IsEquiv w
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
⊢ UniformContinuous (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → WithVal w)
have h1 : UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)
Tactic: have h1 := IsEquiv.uniformContinuous_equiv (hval := Valued.mk' w) rfl 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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)
⊢ UniformContinuous (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → WithVal w)
have h2 : UniformContinuous (α := R) (β := WithVal w) (⇑(equiv w).symm : (a : R) → WithVal w)
Tactic: have h2 := IsEquiv.uniformContinuous_equiv_symm (hval := Valued.mk' v) rfl 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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)
h2 : UniformContinuous (α := R) (β := WithVal w) (⇑(equiv w).symm : (a : R) → WithVal w)
⊢ UniformContinuous (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → WithVal w)
have hR : UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
Tactic: have hR : @UniformContinuous R R (Valued.mk' w).toUniformSpace (Valued.mk' v).toUniformSpace
      (RingHom.id R) := h.uniformContinuous
-- 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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
h1 : UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)
h2 : UniformContinuous (α := R) (β := WithVal w) (⇑(equiv w).symm : (a : R) → WithVal w)
hR : UniformContinuous (α := R) (β := R) (⇑(RingHom.id R) : (a : R) → R)
⊢ UniformContinuous (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → WithVal w)
have apply : UniformContinuous (α := R) (β := WithVal w) (⇑(RingEquiv.trans (RingEquiv.refl R) (equiv w).symm) : (a : R) → WithVal w)
Tactic: apply @UniformContinuous.comp (WithVal v) R (WithVal w) _ (Valued.mk' w).toUniformSpace _
    ((RingEquiv.refl R).trans (WithVal.equiv w).symm) (WithVal.equiv v) ?_ h1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
K : Type u_7
inst : Field K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : Function.Surjective.{u_7 + 1, u_8 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀ˣ
⊢ ∃ (r : K) (s : K),
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) = (↑γ : Γ₀)
have obtain : ∀ (r : K) (hr : (v : (a : K) → Γ₀) r = (↑γ : Γ₀)),
  ∃ (r : K) (s : K),
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) = (↑γ : Γ₀)
Tactic: obtain ⟨r, hr⟩ := hv γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
K : Type u_7
inst : Field K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ValueGroup₀ v)ˣ
⊢ ∃ (r : K) (s : K),
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
            ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
            ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) s : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
have obtain : ∀ (r : K)
  (hr :
    ((restrict₀ v : MonoidWithZeroHom.{u_7, u_8} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) r =
      (↑γ : ValueGroup₀ v)),
  ∃ (r : K) (s : K),
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
      LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ∧
        HDiv.hDiv (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
            ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
            ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) s : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
          (↑γ : ValueGroup₀ v)
Tactic: obtain ⟨r, hr⟩ := MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective v γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
K : Type u_7
inst : Field K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ValueGroup₀ v)ˣ
r : K
hr : ((restrict₀ v : MonoidWithZeroHom.{u_7, u_8} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) r = (↑γ : ValueGroup₀ v)
⊢ LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) ∧
      HDiv.hDiv (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) r : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((v.restrict : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) 1 : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) =
        (↑γ : ValueGroup₀ v)
have simp : LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
Tactic: simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
K : Type u_7
inst : Field K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ValueGroup₀ v)ˣ
r : K
hr : ((restrict₀ v : MonoidWithZeroHom.{u_7, u_8} K (ValueGroup₀ v)) : (a : K) → ValueGroup₀ v) r = (↑γ : ValueGroup₀ v)
⊢ LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
have rw : 0 < (↑γ : ValueGroup₀ v)
Tactic: rw [← map_zero v, ← embedding_restrict₀,  ← embedding_restrict₀ r, hr,
      embedding_strictMono.lt_iff_lt, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : UniformSpace.Completion (WithVal v)
⊢ LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
        (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
      ((Valuation.restrict Valued.v :
            (a : UniformSpace.Completion (WithVal v)) →
              ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
          x :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
      (1 :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
have rw : LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
  LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_le_one_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (hypothesis)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
⊢ IsClosed.{u_7} (X := UniformSpace.Completion (WithVal v))
    {a : UniformSpace.Completion (WithVal v) |
      LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : v.Completion) → Γ₀) a : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_6} (α := Γ₀')
          ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
              ((mapEquiv h.uniformEquiv :
                    (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
                  a :
                UniformSpace.Completion (WithVal w)) :
            Γ₀')
          (1 : Γ₀')}
have h1 : ∀ (x : UniformSpace.Completion (WithVal v)),
  LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
        (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
      ((Valuation.restrict Valued.v :
            (a : UniformSpace.Completion (WithVal v)) →
              ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
          x :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
      (1 :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
Tactic: have h1 (x : UniformSpace.Completion (WithVal v)) :
      Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1 := by rw [restrict_le_one_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 :
  ∀ (x : UniformSpace.Completion (WithVal v)),
    LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α :=
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        ((Valuation.restrict Valued.v :
              (a : UniformSpace.Completion (WithVal v)) →
                ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
            x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        (1 :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
⊢ IsClosed.{u_7} (X := UniformSpace.Completion (WithVal v))
    {a : UniformSpace.Completion (WithVal v) |
      LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : v.Completion) → Γ₀) a : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_6} (α := Γ₀')
          ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
              ((mapEquiv h.uniformEquiv :
                    (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
                  a :
                UniformSpace.Completion (WithVal w)) :
            Γ₀')
          (1 : Γ₀')}
have hp : IsClosed.{u_7} (X := UniformSpace.Completion (WithVal v))
  {a : UniformSpace.Completion (WithVal v) |
    LE.le.{u_5} (α :=
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        ((Valuation.restrict Valued.v :
              (a : UniformSpace.Completion (WithVal v)) →
                ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
            a :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        (1 :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀)) ↔
      LE.le.{u_6} (α := Γ₀')
        ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
            ((mapEquiv h.uniformEquiv : (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
                a :
              UniformSpace.Completion (WithVal w)) :
          Γ₀')
        (1 : Γ₀')}
Tactic: simp_rw [h1]