awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 :
  ∀ (x : UniformSpace.Completion (WithVal v)),
    LE.le.{u_5} (α := Γ₀) ((Valued.v : (a : UniformSpace.Completion (WithVal v)) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
      LE.le.{u_5} (α :=
        ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
          (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        ((Valuation.restrict Valued.v :
              (a : UniformSpace.Completion (WithVal v)) →
                ValueGroup₀ (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
            x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
        (1 :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_7, u_5} (UniformSpace.Completion (WithVal v)) Γ₀)
            (↑Valued.v : UniformSpace.Completion (WithVal v) →*₀ Γ₀))
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} (α :=
      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)
have 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 : Γ₀')
Tactic: rw [restrict_le_one_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : v.Completion
⊢ 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 : Γ₀')
have 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 : Γ₀')}
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst_2 : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : 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 : Γ₀')}
⊢ 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 : Γ₀')
have 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 : Γ₀')
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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 : Γ₀)
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)
have 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)
Tactic: simp only [(hasBasis_nhds_zero _ _).tendsto_right_iff, mem_setOf_eq, map_pow, eventually_atTop,
    forall_const]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨n, hn⟩ := exists_pow_lt₀ hx
    (Units.map (MonoidWithZeroHom.ValueGroup₀.embedding (f := v)) y)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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)
have 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)
Tactic: refine ⟨n, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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
⊢ 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)
have rw : LT.lt.{u_2} (α := Γ₀) ((Valued.v : (a : R) → Γ₀) (x ^ m) : Γ₀)
  ((MonoidWithZeroHom.ValueGroup₀.embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → Γ₀)
      (↑y : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
    Γ₀)
Tactic: rw [← map_pow, Valuation.restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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) :
      Γ₀)
have refine : (Valued.v : (a : R) → Γ₀) (x ^ m) ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n
Tactic: refine hn.trans_le' ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
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
⊢ (Valued.v : (a : R) → Γ₀) (x ^ m) ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n
have rw : HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) m ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n
Tactic: rw [map_pow]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Valued R (WithZero (Multiplicative ℤ))
x : R
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)
have refine : LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
Tactic: refine tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Valued R (WithZero (Multiplicative ℤ))
x : R
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
have rw : LT.lt (α := ℤ) (-1) 0
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Valued R (WithZero (Multiplicative ℤ))
x : R
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ (n : ℕ),
    HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        n <
      (↑γ : WithZero (Multiplicative ℤ))
have refine : LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
Tactic: refine exists_pow_lt₀ (hx.trans_lt ?_) _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithZeroMulInt (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : Valued R (WithZero (Multiplicative ℤ))
x : R
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
have rw : LT.lt (α := ℤ) (-1) 0
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ Eq.{u_2 + 1} (α := (x : Γ₀) → Filter Γ₀) 𝓝
    (update (β := fun (a : Γ₀) ↦ Filter Γ₀) pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)))
have rw : LE.le.{u_2} (α := Filter Γ₀) (pure 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
Tactic: rw [nhds_nhdsAdjoint, sup_of_le_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ Eq.{u_2 + 1} (α := Filter Γ₀) (𝓝 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
have rw : Eq.{u_2 + 1} (α := Filter Γ₀) (update (β := fun (a : Γ₀) ↦ Filter Γ₀) pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) 0)
  (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
Tactic: rw [nhds_eq_update, update_self]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
rw :
  Eq.{u_2 + 1} (α := Filter Γ₀) (update (β := fun (a : Γ₀) ↦ Filter Γ₀) pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) 0)
    (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
⊢ Eq.{u_2 + 1} (α := Filter Γ₀) (𝓝 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
have rw₁ : Eq.{u_2 + 1} (α := Filter Γ₀) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
Tactic: rw [nhds_eq_update, update_self]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ HasBasis (𝓝 0) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio
have rw : HasBasis (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio
Tactic: rw [nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ HasBasis (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio
have refine : DirectedOn.{u_2} (α := Γ₀) (Iio ⁻¹'o fun (x1 x2 : Set Γ₀) ↦ x1 ≥ x2) fun (γ : Γ₀) ↦ γ = 0 → False
Tactic: refine hasBasis_biInf_principal ?_ ⟨1, one_ne_zero⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (𝓝 x).HasBasis (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}
have rw : HasBasis (pure x) (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}
Tactic: rw [nhds_of_ne_zero h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
have rw : Tendsto f l (pure γ) ↔ ∀ᶠ (x : α) in l, f x = γ
Tactic: rw [nhds_of_ne_zero h, tendsto_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
rw : Tendsto f l (pure γ) ↔ ∀ᶠ (x : α) in l, f x = γ
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
have rw₁ : (∀ᶠ (x : α) in l, f x = γ) ↔ ∀ᶠ (x : α) in l, f x = γ
Tactic: rw [nhds_of_ne_zero h, tendsto_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁
have inl : ∀ (h : 0 < γ₂), Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio γ₂)
Tactic: rcases eq_or_ne γ₁ 0 with (rfl | h₀)
Cleared hypotheses: γ₁, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
inl : ∀ (h : 0 < γ₂), Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio γ₂)
⊢ Iio γ₂ ∈ 𝓝 γ₁
have inr : ∀ (h₀ : γ₁ ≠ 0), Iio γ₂ ∈ 𝓝 γ₁
Tactic: rcases eq_or_ne γ₁ 0 with (rfl | h₀)
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsOpen[topologicalSpace] s ↔ 0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Iio γ ⊆ s
have rw : ((0 ∈ s → Membership.mem (γ := Filter Γ₀) (𝓝 0) s) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔
  0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Iio γ ⊆ s
Tactic: rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ IsClosed[instTopologicalSpaceProd] {p : Γ₀ × Γ₀ | p.1 ≤ p.2}
have simp : ∀ (x : Γ₀ × Γ₀), Membership.mem (γ := Set (Γ₀ × Γ₀)) {a : Γ₀ × Γ₀ | a.2 < a.1} x → {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ 𝓝 x
Tactic: simp only [← isOpen_compl_iff, compl_setOf, not_le, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ 𝓝 (a, b)
have rw : {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ map (Prod.mk a) (𝓝 b)
Tactic: rw [nhds_prod_eq, nhds_of_ne_zero (zero_le'.trans_lt hab).ne', pure_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have pos : ∀ (hs : 0 ∈ s), Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: by_cases hs : 0 ∈ s
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
pos : ∀ (hs : 0 ∈ s), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have neg : ∀ (hs : 0 ∉ s), Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: by_cases hs : 0 ∈ s
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (hypothesis)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have ht : 0 ∉ t
Tactic: have ht : 0 ∉ t := fun ht => disjoint_left.1 h₁ (subset_closure hs) ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∈ s
ht : 0 ∉ t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have pos : Disjoint (𝓝ˢ s) (𝓟 t)
Tactic: rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have neg : Disjoint (𝓟 s) (𝓝ˢ t)
Tactic: rwa [(isOpen_iff.2 (.inl hs)).nhdsSet_eq, disjoint_principal_nhdsSet]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2
have simp : ∀ (x : Γ₀ × Γ₀), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 x) (𝓝 (x.1 * x.2))
Tactic: simp only [continuous_iff_continuousAt, ContinuousAt]