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 Γ₀'
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
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)
⊢ ∃ (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:
simp only [Set.mem_setOf_eq, RingHom.id_apply]

Premises used: RingHom.id_apply, Set.mem_setOf_eq
-- 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 ⋯
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
⊢ 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

Premises used: Units.val, Valuation.IsEquiv.orderMonoidIso, DFunLike.coe
-- 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 ⋯
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)
⊢ y₀ ≠ 0

Tactic:
simp [hy₀_def]
-- 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 ⋯
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)
⊢ y₀ ≠ 0

Tactic:
have hy₀_ne_zero : y₀ ≠ 0 := by simp [hy₀_def]
-- 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 ⋯
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
⊢ 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

Premises used: Units.mk0
-- 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 ⋯
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
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)
⊢ ∃ (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:
use y
-- 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
⊢ 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)
-- 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
hcomp : WithVal.congr v w (RingEquiv.refl R) = WithVal.congr v w (RingEquiv.refl R)
⊢ UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)

Tactic:
have h1 := IsEquiv.uniformContinuous_equiv (hval := Valued.mk' w) rfl 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
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 (α := R) (β := WithVal w) (⇑(equiv w).symm : (a : R) → WithVal w)

Tactic:
have h2 := IsEquiv.uniformContinuous_equiv_symm (hval := Valued.mk' v) rfl 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
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 (α := 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
-- 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
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)
apply :
  UniformContinuous (α := R) (β := WithVal w)
    (⇑(RingEquiv.trans (RingEquiv.refl R) (equiv w).symm) : (a : R) → WithVal w)
⊢ UniformContinuous (α := WithVal v) (β := WithVal w)
    (⇑(WithVal.congr v w (RingEquiv.refl R)) : (a : WithVal v) → 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

Premises used: UniformContinuous.comp
-- 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
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 (α := R) (β := WithVal w)
    (⇑(RingEquiv.trans (RingEquiv.refl R) (equiv w).symm) : (a : R) → WithVal w)

Tactic:
@UniformContinuous.comp R R (WithVal w) (Valued.mk' w).toUniformSpace
       (Valued.mk' v).toUniformSpace _ (WithVal.equiv w).symm (RingEquiv.refl R) h2 hR

Premises used: UniformContinuous.comp
-- 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
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 (α := R) (β := WithVal w)
    (⇑(RingEquiv.trans (RingEquiv.refl R) (equiv w).symm) : (a : R) → WithVal w)

Tactic:
exact @UniformContinuous.comp R R (WithVal w) (Valued.mk' w).toUniformSpace
       (Valued.mk' v).toUniformSpace _ (WithVal.equiv w).symm (RingEquiv.refl R) h2 hR

Premises used: UniformContinuous.comp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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) → Γ₀)
γ : Γ₀ˣ
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 : Γ₀) = (↑γ : Γ₀)
⊢ ∃ (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 γ

Premises used: Units.val
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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
hr : (v : (a : K) → Γ₀) r = (↑γ : Γ₀)
⊢ LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ∧
    LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) ∧
      HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ((v : (a : K) → Γ₀) 1 : Γ₀) = (↑γ : Γ₀)

Tactic:
simp [hr]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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
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:
exact ⟨r, 1, by simp [hr]⟩
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
K : Type u_7
inst : Field K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ValueGroup₀ v)ˣ
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)
⊢ ∃ (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 γ

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
simp : LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ 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)

Tactic:
simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]

Premises used: and_true, and_self, zero_lt_one, Valuation.restrict_def, map_one, div_one
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
rw : 0 < (↑γ : ValueGroup₀ v)
⊢ LT.lt.{u_8} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
rw [← map_zero v, ← embedding_restrict₀,  ← embedding_restrict₀ r, hr,
      embedding_strictMono.lt_iff_lt, map_zero]

Premises used: StrictMono.lt_iff_lt, map_zero, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
⊢ 0 < (↑γ : ValueGroup₀ v)

Tactic:
WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ)

Premises used: Iff.mpr, WithZero.pos_iff_ne_zero, Units.ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
⊢ 0 < (↑γ : ValueGroup₀ v)

Tactic:
refine WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ)

Premises used: Iff.mpr, WithZero.pos_iff_ne_zero, Units.ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
⊢ ∃ (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:
exact ⟨r, 1, by
    simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]
    rw [← map_zero v, ← embedding_restrict₀,  ← embedding_restrict₀ r, hr,
      embedding_strictMono.lt_iff_lt, map_zero]
    refine WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ)⟩
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
⊢ ∃ (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:
classical
  exact ⟨r, 1, by
    simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]
    rw [← map_zero v, ← embedding_restrict₀,  ← embedding_restrict₀ r, hr,
      embedding_strictMono.lt_iff_lt, map_zero]
    refine WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ)⟩
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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)
rw 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 : Γ₀)
⊢ 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:
rw [restrict_le_one_iff]

Premises used: Valuation.restrict_le_one_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
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) →*₀ Γ₀))

Tactic:
have h1 (x : UniformSpace.Completion (WithVal v)) :
      Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1 := by rw [restrict_le_one_iff]