awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
y : ValueGroup₀ v
b : ↥(valueGroup v)
⊢ (WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
        (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
            (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
          (↑b : WithZero ↥(valueGroup v)) :
        WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)) =
    (↑b : WithZero ↥(valueGroup v))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
y : ValueGroup₀ v
⊢ (WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
        (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
            (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
          y :
        WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)) =
    y

Tactic:
match y with
    | 0 => simp
    | .coe b => simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ ∀ (x y : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v),
    (WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (x * y) =
      HMul.hMul (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
              (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
            x :
          WithZero ↥(valueGroup v))
        ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
              (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
            y :
          WithZero ↥(valueGroup v))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
a b : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
⊢ LE.le (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          0 :
        WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          0 :
        WithZero ↥(valueGroup v)) ↔
    LE.le.{u_2} (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) 0 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
a b : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
val : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
⊢ LE.le (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          0 :
        WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (↑val : WithZero ↥(valueGroup Valued.v)) :
        WithZero ↥(valueGroup v)) ↔
    0 ≤ (↑val : WithZero ↥(valueGroup Valued.v))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
a b : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
val : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
⊢ LE.le (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (↑val : WithZero ↥(valueGroup Valued.v)) :
        WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          0 :
        WithZero ↥(valueGroup v)) ↔
    (↑val : WithZero ↥(valueGroup Valued.v)) ≤ 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
a_1 b_1 : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
a b : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
⊢ LE.le (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (↑a : WithZero ↥(valueGroup Valued.v)) :
        WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (↑b : WithZero ↥(valueGroup Valued.v)) :
        WithZero ↥(valueGroup v)) ↔
    (↑a : WithZero ↥(valueGroup Valued.v)) ≤ (↑b : WithZero ↥(valueGroup Valued.v))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
a b : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
⊢ LE.le (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          a :
        WithZero ↥(valueGroup v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          b :
        WithZero ↥(valueGroup v)) ↔
    a ≤ b

Tactic:
match a, b with
    | 0, 0 => simp
    | 0, .coe _ => simp
    | .coe _, 0 => simp
    | .coe a, .coe b => simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
simp :
  Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (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.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
⊢ Eq (α := ValueGroup₀ v)
    ((valueGroupOrderIso₀ v : (a : ValueGroup₀ Valued.v) → ValueGroup₀ v)
        ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) b :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_3, u_2} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) :
      ValueGroup₀ v)
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) b.ofVal : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
simp [Valued.v.restrict_def, restrict₀_apply, ← apply_ofVal, v.restrict_def]

Premises used: WithVal.apply_ofVal, Valued.v, Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (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.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)

Tactic:
simp [hb]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
hb : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (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.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)

Tactic:
simp [hb]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
simp :
  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)
⊢ Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    (((valueGroupOrderIso₀ v).symm : (a : ValueGroup₀ v) → ValueGroup₀ Valued.v)
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) b : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v b) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_3, u_2} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))

Tactic:
simp [Valued.v.restrict_def, restrict₀_apply, ← apply_ofVal, v.restrict_def]

Premises used: WithVal.apply_ofVal, Valued.v, Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
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) ⋯) :
            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)

Tactic:
simp [hb]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
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) ⋯) :
            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)

Tactic:
simp [hb]
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ StrictMono (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) (β := ValueGroup₀ v)
    (⇑(valueGroupOrderIso₀ v) : (a : ValueGroup₀ Valued.v) → ValueGroup₀ v)

Tactic:
WithZero.map'_strictMono (strictMono_valueGroupEquiv v)

Premises used: WithZero.map'_strictMono, Set.Mem, setOf, WithZero.recZeroCoe, WithVal.strictMono_valueGroupEquiv
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ StrictMono (α := ValueGroup₀ v) (β := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    (⇑(valueGroupOrderIso₀ v).symm : (a : ValueGroup₀ v) → ValueGroup₀ Valued.v)

Tactic:
WithZero.map'_strictMono (strictMono_valueGroupEquiv_symm v)

Premises used: WithZero.map'_strictMono, Set.Mem, setOf, WithVal.strictMono_valueGroupEquiv_symm, WithZero.recZeroCoe
-- 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
x : WithVal v
⊢ (h.orderRingIso : (a : WithVal v) → WithVal w) x = toVal w x.ofVal

Tactic:
rfl

Premises used: 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
x : WithVal w
⊢ (h.orderRingIso.symm : (a : WithVal w) → WithVal v) x = toVal v x.ofVal

Tactic:
rfl

Premises used: 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
⊢ UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)

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 : v.IsEquiv w
refine : ContinuousAt (X := WithVal v) (Y := R) (⇑(equiv v) : (a : WithVal v) → R) 0
⊢ UniformContinuous (α := WithVal v) (β := R) (⇑(equiv v) : (a : WithVal v) → R)

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 : v.IsEquiv w
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)
⊢ ContinuousAt (X := WithVal v) (Y := R) (⇑(equiv v) : (a : WithVal v) → R) 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 : v.IsEquiv w
γ : (ValueGroup₀ (F := Valuation R Γ₀') Valued.v)ˣ
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)
⊢ ∃ (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 γ

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 : 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)
⊢ 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 →*₀ Γ₀)) ≠
    0

Tactic:
simp [Valuation.restrict_def, restrict₀_eq_zero_iff, (eq_zero h (r := r)).ne, ← hv,
      (eq_zero h (r := s)).ne, hr₀.ne', hs₀.ne']

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, LT.lt.ne', Valuation.restrict_def, Valuation.IsEquiv.eq_zero, Iff.ne