awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : 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
⊢ toVal v y = x

Tactic:
have hy : toVal v y = x := 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 Γ₀'
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
⊢ 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:
simp [restrict_pos_iff, h.pos_iff, ← hv, hs₀]

Premises used: Valuation.IsEquiv.pos_iff, Valuation.restrict_pos_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : 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
⊢ 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₀]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : 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 →*₀ Γ₀))
⊢ v.restrict.IsEquiv w.restrict

Tactic:
have h' : v.restrict.IsEquiv w.restrict := h.restrict
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ UniformContinuous (α := R) (β := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v)

Tactic:
uniformContinuous_of_continuousAt_zero _ ?_

Premises used: uniformContinuous_of_continuousAt_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
refine : ContinuousAt (X := R) (Y := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v) 0
⊢ UniformContinuous (α := R) (β := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v)

Tactic:
refine uniformContinuous_of_continuousAt_zero _ ?_

Premises used: uniformContinuous_of_continuousAt_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
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)
⊢ ContinuousAt (X := R) (Y := WithVal v) (⇑(equiv v).symm : (a : R) → WithVal v) 0

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

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, Valued.hasBasis_nhds_zero, map_zero, forall_const, true_and
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
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)
⊢ ∃ (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 γ

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

Tactic:
have h' : w.restrict.IsEquiv v.restrict := h.restrict
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
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
simp :
  ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r.ofVal : Γ₀) (0 : Γ₀) ∧
    ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) (0 : Γ₀)
⊢ 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

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]

Premises used: WithVal.equiv_apply, MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq, not_or, Valuation.restrict_def, Valuation.IsEquiv.eq_zero, Iff.ne, div_eq_zero_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
⊢ ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r.ofVal : Γ₀) (0 : Γ₀) ∧
    ¬Eq.{u_5 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s.ofVal : Γ₀) (0 : Γ₀)

Tactic:
⟨hr₀.ne', hs₀.ne'⟩

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

Tactic:
exact ⟨hr₀.ne', hs₀.ne'⟩
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ValueGroup₀ (F := Valuation.{u_4, u_5} (WithVal v) Γ₀) Valued.v)ˣ
r s : WithVal v
hr₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)
hs₀ : LT.lt.{u_5} (α := Γ₀) (0 : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) s : Γ₀)
hr :
  HDiv.hDiv (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) (β :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) r :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) s :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_4, u_5} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) =
    (↑γ : ValueGroup₀ Valued.v)
h' : w.restrict.IsEquiv v.restrict
x : R
hx :
  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
h₁ :
  (Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v x) <
    (↑γ : ValueGroup₀ Valued.v)
⊢ 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:
simp only [equiv_symm_apply, Set.mem_setOf_eq]

Premises used: WithVal.equiv_symm_apply, Set.mem_setOf_eq