awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) →*₀ Γ₀))
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 : Γ₀')}
⊢ 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 : Γ₀')}

Tactic:
simp_rw [h1]
-- 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
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))
    {x : 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) →*₀ Γ₀))
              x :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
              (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
          (1 : ValueGroup₀ (F := Valuation.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀) Valued.v) ↔
        LE.le.{u_6} (α :=
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
            (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
          ((Valuation.restrict Valued.v :
                (a : UniformSpace.Completion (WithVal w)) →
                  ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
              (((mapEquiv h.uniformEquiv).toHomeomorph :
                  (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
                x) :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
              (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
          (1 : ValueGroup₀ (F := Valuation.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀') Valued.v)}

Tactic:
(mapEquiv h.uniformEquiv).toHomeomorph.isClosed_setOf_iff
        (Valued.isClopen_closedBall _ one_ne_zero) (Valued.isClopen_closedBall _ one_ne_zero)

Premises used: Valuation.IsEquiv.uniformEquiv, UniformSpace.Completion.mapEquiv, UniformEquiv.toHomeomorph, Homeomorph.isClosed_setOf_iff, one_ne_zero, Valued.isClopen_closedBall
-- 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
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) →*₀ Γ₀))
x : UniformSpace.Completion (WithVal v)
h₁ :
  LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          ((mapEquiv h.uniformEquiv : (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀') ↔
    LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          (((mapEquiv h.uniformEquiv).toHomeomorph :
                (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀')
⊢ LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          ((mapEquiv h.uniformEquiv : (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀') ↔
    LE.le.{u_6} (α :=
      ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
        (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
      ((Valuation.restrict Valued.v :
            (a : UniformSpace.Completion (WithVal w)) →
              ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
          (((mapEquiv h.uniformEquiv).toHomeomorph :
              (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
            x) :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀')
          (↑Valued.v : UniformSpace.Completion (WithVal w) →*₀ Γ₀'))
      (1 : ValueGroup₀ (F := Valuation.{u_7, u_6} (UniformSpace.Completion (WithVal w)) Γ₀') Valued.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
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) →*₀ Γ₀))
x : 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))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀') ↔
    LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          (((mapEquiv h.uniformEquiv).toHomeomorph :
                (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀')

Tactic:
rfl
-- 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
a : WithVal v
⊢ LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : v.Completion) → Γ₀) (↑a : UniformSpace.Completion (WithVal v)) : Γ₀)
      (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 v)) :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀')

Tactic:
simpa [Valued.valuedCompletion_apply] using h.le_one_iff_le_one

Premises used: Valued.valuedCompletion_apply, Valuation.IsEquiv.le_one_iff_le_one
-- 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 : v.Completion
hp :
  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 : Γ₀')}
ih :
  ∀ (a : WithVal v),
    LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : v.Completion) → Γ₀) (↑a : UniformSpace.Completion (WithVal v)) : Γ₀)
        (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 v)) :
              UniformSpace.Completion (WithVal w)) :
          Γ₀')
        (1 : Γ₀')
⊢ LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : v.Completion) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_6} (α := Γ₀')
      ((Valued.v : (a : UniformSpace.Completion (WithVal w)) → Γ₀')
          ((mapEquiv h.uniformEquiv : (a : UniformSpace.Completion (WithVal v)) → UniformSpace.Completion (WithVal w))
              x :
            UniformSpace.Completion (WithVal w)) :
        Γ₀')
      (1 : Γ₀')

Tactic:
induction x using induction_on with
  | hp =>
    have h1 (x : UniformSpace.Completion (WithVal v)) :
      Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1 := by rw [restrict_le_one_iff]
    simp_rw [h1]
    convert!
      (mapEquiv h.uniformEquiv).toHomeomorph.isClosed_setOf_iff
        (Valued.isClopen_closedBall _ one_ne_zero) (Valued.isClopen_closedBall _ one_ne_zero)
    rw [restrict_le_one_iff]
    rfl
  | ih a =>
    simpa [Valued.valuedCompletion_apply] using h.le_one_iff_le_one

Premises used: Valuation.IsEquiv.uniformEquiv, UniformSpace.Completion.mapEquiv, UniformEquiv.toHomeomorph, Homeomorph.isClosed_setOf_iff, Valued.valuedCompletion_apply, Valuation.IsEquiv.le_one_iff_le_one, Valuation.restrict_le_one_iff, one_ne_zero, Valued.isClopen_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst_1 : Field K
inst_2 : NumberField K
v : Valuation K Γ₀
R : Type u_4
inst_3 : CommRing R
inst_4 : Algebra R K
inst_5 : IsIntegralClosure R ℤ K
⊢ IsIntegralClosure.{u_4, 0, u_3} R ℤ (WithVal v)

Tactic:
.of_algEquiv _ (WithVal.algEquiv ℤ v).symm (fun _ ↦ rfl)

Premises used: AlgEquiv.symm, IsIntegralClosure.of_algEquiv, Int, WithVal.algEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
simp :
  ∀ (i : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ (a : ℕ),
      ∀ b ≥ a,
        HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            b <
          (↑i : MonoidWithZeroHom.ValueGroup₀ v)
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)

Tactic:
simp only [(hasBasis_nhds_zero _ _).tendsto_right_iff, mem_setOf_eq, map_pow, eventually_atTop,
    forall_const]

Premises used: Valued.hasBasis_nhds_zero, Set.mem_setOf_eq, map_pow, forall_const, Filter.HasBasis.tendsto_right_iff, Filter.eventually_atTop
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
obtain :
  ∀ (n : ℕ)
    (hn :
      HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
        (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
                (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
              y) :
          Γ₀)),
    ∃ (a : ℕ),
      ∀ b ≥ a,
        HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
            ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
              MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
            b <
          (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          b <
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt₀ hx
    (Units.map (MonoidWithZeroHom.ValueGroup₀.embedding (f := v)) y)

Premises used: exists_pow_lt₀, DFunLike.coe, Units.map
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          b <
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
⟨n, fun m hm ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
refine :
  ∀ (m : ℕ) (hm : m ≥ n),
    HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
        ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
        m <
      (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
          b <
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
refine ⟨n, fun m hm ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
m : ℕ
hm : m ≥ n
rw :
  LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) (x ^ m) : Γ₀)
    ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → Γ₀)
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      Γ₀)
⊢ HPow.hPow (α := MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
      ((Valuation.restrict Valued.v : (a : R) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : R →*₀ Γ₀)) x :
        MonoidWithZeroHom.ValueGroup₀ (F := R →*₀ Γ₀) (↑Valued.v : R →*₀ Γ₀))
      m <
    (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
rw [← map_pow, Valuation.restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding, map_pow
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
m : ℕ
hm : m ≥ n
⊢ LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) (x ^ m) : Γ₀)
    ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → Γ₀)
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      Γ₀)

Tactic:
hn.trans_le' ?_

Premises used: Set.Mem, setOf, LT.lt.trans_le'
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
m : ℕ
hm : m ≥ n
refine : (Valued.v : (a : R) → Γ₀) (x ^ m) ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n
⊢ LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) (x ^ m) : Γ₀)
    ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → Γ₀)
        (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      Γ₀)

Tactic:
refine hn.trans_le' ?_

Premises used: LT.lt.trans_le'
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued R Γ₀
x : R
hx : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
y : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation R Γ₀) Valued.v)ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn :
  HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n <
    (↑((Units.map (↑MonoidWithZeroHom.ValueGroup₀.embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* Γ₀) :
            (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → Γ₀ˣ)
          y) :
      Γ₀)
m : ℕ
hm : m ≥ n
rw : HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) m ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n
⊢ (Valued.v : (a : R) → Γ₀) (x ^ m) ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n

Tactic:
rw [map_pow]

Premises used: map_pow