awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) m ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n

Tactic:
pow_le_pow_right_of_le_one' hx.le hm

Premises used: LT.lt.le, pow_le_pow_right_of_le_one'
-- 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
⊢ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) m ≤ HPow.hPow (α := Γ₀) ((Valued.v : (a : R) → Γ₀) x : Γ₀) n

Tactic:
exact pow_le_pow_right_of_le_one' hx.le hm

Premises used: LT.lt.le, pow_le_pow_right_of_le_one'
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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)

Tactic:
tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)

Premises used: Valued.tendsto_zero_pow_of_v_lt_one, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 ℤ))
refine : LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ x ^ n) atTop (𝓝 0)

Tactic:
refine tendsto_zero_pow_of_v_lt_one (hx.trans_lt ?_)

Premises used: Valued.tendsto_zero_pow_of_v_lt_one, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 ℤ))
rw : LT.lt (α := ℤ) (-1) 0
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1

Tactic:
rw [← exp_zero, exp_lt_exp]

Premises used: WithZero.exp_lt_exp, WithZero.exp_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 (α := ℤ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 ℤ))

Tactic:
exists_pow_lt₀ (hx.trans_lt ?_) _

Premises used: exists_pow_lt₀, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 ℤ))ˣ
refine : LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1
⊢ ∃ (n : ℕ),
    HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((v : Valuation R (WithZero (Multiplicative ℤ))) : (a : R) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        n <
      (↑γ : WithZero (Multiplicative ℤ))

Tactic:
refine exists_pow_lt₀ (hx.trans_lt ?_) _

Premises used: exists_pow_lt₀, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 ℤ))ˣ
rw : LT.lt (α := ℤ) (-1) 0
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-1)) 1

Tactic:
rw [← exp_zero, exp_lt_exp]

Premises used: WithZero.exp_lt_exp, WithZero.exp_zero
-- Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt
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 (α := ℤ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
rw : LE.le.{u_2} (α := Filter Γ₀) (pure 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
⊢ Eq.{u_2 + 1} (α := (x : Γ₀) → Filter Γ₀) 𝓝
    (update (β := fun (a : Γ₀) ↦ Filter Γ₀) pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)))

Tactic:
rw [nhds_nhdsAdjoint, sup_of_le_right]

Premises used: nhds_nhdsAdjoint, sup_of_le_right
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ LE.le.{u_2} (α := Filter Γ₀) (pure 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
le_iInf₂ fun γ hγ ↦ le_principal_iff.2 <| zero_lt_iff.2 hγ

Premises used: Iff.mpr, Filter.le_principal_iff, Set.Mem, setOf, le_iInf₂, zero_lt_iff
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ LE.le.{u_2} (α := Filter Γ₀) (pure 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
exact le_iInf₂ fun γ hγ ↦ le_principal_iff.2 <| zero_lt_iff.2 hγ

Premises used: Iff.mpr, Filter.le_principal_iff, le_iInf₂
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
rw :
  Eq.{u_2 + 1} (α := Filter Γ₀) (update (β := fun (a : Γ₀) ↦ Filter Γ₀) pure 0 (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) 0)
    (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
rw₁ rw₂ : Eq.{u_2 + 1} (α := Filter Γ₀) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
⊢ Eq.{u_2 + 1} (α := Filter Γ₀) (𝓝 0) (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
rw [nhds_eq_update, update_self]

Premises used: Function.update_self, WithZeroTopology.nhds_eq_update
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
rw : HasBasis (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio
⊢ HasBasis (𝓝 0) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio

Tactic:
rw [nhds_zero]

Premises used: WithZeroTopology.nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ HasBasis (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio

Tactic:
hasBasis_biInf_principal ?_ ⟨1, one_ne_zero⟩

Premises used: Filter.hasBasis_biInf_principal, Set.Mem, Exists.intro, one_ne_zero, OfNat.ofNat, Not
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
refine : DirectedOn.{u_2} (α := Γ₀) (Iio ⁻¹'o fun (x1 x2 : Set Γ₀) ↦ x1 ≥ x2) fun (γ : Γ₀) ↦ γ = 0 → False
⊢ HasBasis (⨅ (γ : Γ₀), ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) (fun (γ : Γ₀) ↦ γ ≠ 0) Iio

Tactic:
refine hasBasis_biInf_principal ?_ ⟨1, one_ne_zero⟩

Premises used: Filter.hasBasis_biInf_principal, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ DirectedOn.{u_2} (α := Γ₀) (Iio ⁻¹'o fun (x1 x2 : Set Γ₀) ↦ x1 ≥ x2) fun (γ : Γ₀) ↦ γ = 0 → False

Tactic:
directedOn_iff_directed.2 (Monotone.directed_ge fun a b hab => Iio_subset_Iio hab)

Premises used: Iff.mpr, Monotone.directed_ge, Set.Iio_subset_Iio, directedOn_iff_directed
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
⊢ DirectedOn.{u_2} (α := Γ₀) (Iio ⁻¹'o fun (x1 x2 : Set Γ₀) ↦ x1 ≥ x2) fun (γ : Γ₀) ↦ γ = 0 → False

Tactic:
exact directedOn_iff_directed.2 (Monotone.directed_ge fun a b hab => Iio_subset_Iio hab)

Premises used: Iff.mpr, Monotone.directed_ge, directedOn_iff_directed
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
hγ : γ ≠ 0
⊢ Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio γ)

Tactic:
hasBasis_nhds_zero.mem_of_mem hγ

Premises used: WithZeroTopology.hasBasis_nhds_zero, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio (↑γ : Γ₀))

Tactic:
Iio_mem_nhds_zero γ.ne_zero

Premises used: Units.ne_zero, WithZeroTopology.Iio_mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀

Tactic:
simp [nhds_zero]

Premises used: WithZeroTopology.nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
h₀ : γ ≠ 0
⊢ 𝓝 γ = pure γ

Tactic:
nhds_nhdsAdjoint_of_ne _ h₀

Premises used: nhds_nhdsAdjoint_of_ne
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ 𝓝 (↑γ : Γ₀) = pure (↑γ : Γ₀)

Tactic:
nhds_of_ne_zero γ.ne_zero

Premises used: Units.ne_zero, WithZeroTopology.nhds_of_ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ {(↑γ : Γ₀)} ∈ 𝓝 (↑γ : Γ₀)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
rw : HasBasis (pure x) (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}
⊢ (𝓝 x).HasBasis (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}

Tactic:
rw [nhds_of_ne_zero h]

Premises used: WithZeroTopology.nhds_of_ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}

Tactic:
hasBasis_pure _

Premises used: Filter.hasBasis_pure
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ HasBasis (pure x) (fun (x : Unit) ↦ True) fun (x_1 : Unit) ↦ {x}

Tactic:
exact hasBasis_pure _

Premises used: Filter.hasBasis_pure
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ (𝓝 (↑γ : Γ₀)).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ {(↑γ : Γ₀)}

Tactic:
hasBasis_nhds_of_ne_zero γ.ne_zero

Premises used: WithZeroTopology.hasBasis_nhds_of_ne_zero, Units.ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
rw : Tendsto f l (pure γ) ↔ ∀ᶠ (x : α) in l, f x = γ
rw₁ rw₂ : (∀ᶠ (x : α) in l, f x = γ) ↔ ∀ᶠ (x : α) in l, f x = γ
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ

Tactic:
rw [nhds_of_ne_zero h, tendsto_pure]

Premises used: WithZeroTopology.nhds_of_ne_zero, Filter.tendsto_pure
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ₀ : Γ₀ˣ
⊢ Tendsto f l (𝓝 (↑γ₀ : Γ₀)) ↔ ∀ᶠ (x : α) in l, f x = (↑γ₀ : Γ₀)

Tactic:
tendsto_of_ne_zero γ₀.ne_zero

Premises used: WithZeroTopology.tendsto_of_ne_zero, Units.ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
inl : ∀ (h : 0 < γ₂), Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio γ₂)
inr : ∀ (h₀ : γ₁ ≠ 0), Iio γ₂ ∈ 𝓝 γ₁
⊢ Iio γ₂ ∈ 𝓝 γ₁

Tactic:
rcases eq_or_ne γ₁ 0 with (rfl | h₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ₂ : Γ₀
h : 0 < γ₂
⊢ Membership.mem (γ := Filter Γ₀) (𝓝 0) (Iio γ₂)

Tactic:
simp [*, h.ne', Iio_mem_nhds_zero]

Premises used: LT.lt.ne', WithZeroTopology.Iio_mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
h₀ : γ₁ ≠ 0
⊢ Iio γ₂ ∈ 𝓝 γ₁

Tactic:
simp [*, h.ne', Iio_mem_nhds_zero]

Premises used: LT.lt.ne', WithZeroTopology.Iio_mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
rw :
  ((0 ∈ s → Membership.mem (γ := Filter Γ₀) (𝓝 0) s) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔
    0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Iio γ ⊆ s
⊢ IsOpen[topologicalSpace] s ↔ 0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
rw [isOpen_iff_mem_nhds, ← and_forall_ne (0 : Γ₀)]

Premises used: and_forall_ne, isOpen_iff_mem_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → Membership.mem (γ := Filter Γ₀) (𝓝 0) s) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔
    0 ∉ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
simp +contextual [nhds_of_ne_zero, imp_iff_not_or,
    hasBasis_nhds_zero.mem_iff]

Premises used: Filter.HasBasis.mem_iff, WithZeroTopology.hasBasis_nhds_zero, imp_iff_not_or, WithZeroTopology.nhds_of_ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsClosed[topologicalSpace] s ↔ 0 ∈ s ∨ ∃ (γ : Γ₀), γ ≠ 0 ∧ s ⊆ Ici γ

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici,
    compl_subset_compl]

Premises used: Classical.not_not, Set.compl_subset_compl, WithZeroTopology.isOpen_iff, Set.compl_Ici, isOpen_compl_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
a : Γ₀
⊢ IsOpen[topologicalSpace] (Iio a)

Tactic:
isOpen_iff.mpr <| imp_iff_not_or.mp fun ha => ⟨a, ne_of_gt ha, Subset.rfl⟩

Premises used: Iff.mpr, ne_of_gt, imp_iff_not_or, Set.Subset.rfl, WithZeroTopology.isOpen_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
simp :
  ∀ (x : Γ₀ × Γ₀), Membership.mem (γ := Set (Γ₀ × Γ₀)) {a : Γ₀ × Γ₀ | a.2 < a.1} x → {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ 𝓝 x
⊢ IsClosed[instTopologicalSpaceProd] {p : Γ₀ × Γ₀ | p.1 ≤ p.2}

Tactic:
simp only [← isOpen_compl_iff, compl_setOf, not_le, isOpen_iff_mem_nhds]

Premises used: not_le, isOpen_iff_mem_nhds, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
rw : {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ map (Prod.mk a) (𝓝 b)
⊢ {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ 𝓝 (a, b)

Tactic:
rw [nhds_prod_eq, nhds_of_ne_zero (zero_le'.trans_lt hab).ne', pure_prod]

Premises used: Filter.pure_prod, WithZeroTopology.nhds_of_ne_zero, LT.lt.ne', zero_le', nhds_prod_eq, LE.le.trans_lt
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ map (Prod.mk a) (𝓝 b)

Tactic:
Iio_mem_nhds hab

Premises used: Set.Mem, WithZeroTopology.Iio_mem_nhds, setOf, Set.preimage, Set.Iio
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a : Γ₀ × Γ₀ | a.2 < a.1} ∈ map (Prod.mk a) (𝓝 b)

Tactic:
exact Iio_mem_nhds hab

Premises used: WithZeroTopology.Iio_mem_nhds
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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)
neg : ∀ (hs : 0 ∉ s), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by_cases hs : 0 ∈ s
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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
⊢ 0 ∉ t

Tactic:
have ht : 0 ∉ t := fun ht => disjoint_left.1 h₁ (subset_closure hs) ht
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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
pos : Disjoint (𝓝ˢ s) (𝓟 t)
pos₁ pos₂ pos₃ pos₄ : Disjoint s (closure[topologicalSpace] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]

Premises used: Iff.mpr, disjoint_nhdsSet_principal, WithZeroTopology.isOpen_iff, Or.inl, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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
neg : Disjoint (𝓟 s) (𝓝ˢ t)
neg₁ neg₂ neg₃ neg₄ : Disjoint (closure[topologicalSpace] s) t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rwa [(isOpen_iff.2 (.inl hs)).nhdsSet_eq, disjoint_principal_nhdsSet]

Premises used: Iff.mpr, WithZeroTopology.isOpen_iff, disjoint_principal_nhdsSet, Or.inl, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
simp : ∀ (x : Γ₀ × Γ₀), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 x) (𝓝 (x.1 * x.2))
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt]

Premises used: ContinuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
inr :
  ∀ (this : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2)))
    (hle : ¬x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
wlog : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
wlog hle : x ≤ y generalizing x y
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
⊢ Tendsto ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ Prod.swap) (𝓝 (x, y)) (𝓝 ((y, x).1 * (y, x).2))

Tactic:
have := (this y x (le_of_not_ge hle)).comp (continuous_swap.tendsto (x, y))
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this_1 : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
this : Tendsto ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ Prod.swap) (𝓝 (x, y)) (𝓝 ((y, x).1 * (y, x).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
simpa only [mul_comm, Function.comp_def, Prod.swap] using this

Premises used: Function.comp_def, mul_comm, Prod.swap
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
inl : ∀ (hle : 0 ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
inr : ∀ (hx : x ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
inl :
  ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
    Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
inl₁ : ∀ (hy : y ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
inl :
  ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
    Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
inl₁ : ∀ (hle : 0 ≤ y) (hy : y ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
inr : ∀ (hx : x ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]

Premises used: eq_or_ne, OfNat.ofNat, rfl