awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0

Tactic:
exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩

Premises used: Or.inr
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
refine_1 :
  ∀ (n : ℕ) (h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.ofNat n) atTop (𝓝 d)),
    Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0
refine_1₁ :
  ∀ (n : ℕ) (h : Tendsto (fun (x : 𝕜) ↦ c * x ^ Int.negSucc n) atTop (𝓝 d)),
    Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Tactic:
cases n with
    | ofNat n =>
      left
      simpa [tendsto_const_mul_pow_nhds_iff hc] using h
    | negSucc n =>
      have hn := Int.negSucc_lt_zero n
      exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩

Premises used: tendsto_const_mul_pow_nhds_iff, Or.inr
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
refine_2 : ∀ (h : n = 0 ∧ c = d), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
refine_2₁ : ∀ (h : n < 0 ∧ d = 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
rcases h with h | h
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
refine_2 : Tendsto (fun (x : 𝕜) ↦ d) atTop (𝓝 d)
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
simp only [h.left, h.right, zpow_zero, mul_one]

Premises used: zpow_zero, And.right, And.left, mul_one
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ d) atTop (𝓝 d)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ d) atTop (𝓝 d)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1

Premises used: Eq.rec, And.right, And.left, tendsto_const_mul_zpow_atTop_zero, Eq.symm
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ IsTopologicalDivisionRing 𝕜

Tactic:
⟨⟩

Premises used: IsTopologicalDivisionRing.mk
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
rw : Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0)) (𝓝 0 ⊓ 𝓟 (Ioi 0))
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝[>] 0)) (𝓝[>] 0)

Tactic:
rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi₀ _ hx, zero_div]

Premises used: Set.preimage_const_mul_Ioi₀, nhdsWithin, zero_div, Filter.comap_inf, Filter.comap_principal
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
e_a : Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0)) (𝓝 0)
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0)) (𝓝 0 ⊓ 𝓟 (Ioi 0))

Tactic:
congr 1
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0)) (𝓝 0)

Tactic:
((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_

Premises used: Homeomorph.mulLeft₀, Homeomorph.comap_nhds_eq, LT.lt.ne', Eq.trans
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
e_a : Eq (α := Filter 𝕜) (𝓝 ((Homeomorph.symm (Homeomorph.mulLeft₀ x ⋯) : (a : 𝕜) → 𝕜) 0) : Filter 𝕜) (𝓝 0 : Filter 𝕜)
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0)) (𝓝 0)

Tactic:
refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_

Premises used: Homeomorph.mulLeft₀, Homeomorph.comap_nhds_eq, LT.lt.ne', Eq.trans
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ Eq (α := Filter 𝕜) (𝓝 ((Homeomorph.symm (Homeomorph.mulLeft₀ x ⋯) : (a : 𝕜) → 𝕜) 0) : Filter 𝕜) (𝓝 0 : Filter 𝕜)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
rw : ∀ᶠ (ε : 𝕜) in comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝[>] 0), p (x * ε)
⊢ ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p (x * ε)

Tactic:
rw [← comap_mulLeft_nhdsGT_zero hx]

Premises used: comap_mulLeft_nhdsGT_zero
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝[>] 0), p (x * ε)

Tactic:
h.comap fun ε => x * ε

Premises used: HMul.hMul, Filter.Eventually.comap
-- Module: Mathlib.Topology.Algebra.Order.Field
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝[>] 0), p (x * ε)

Tactic:
exact h.comap fun ε => x * ε

Premises used: HMul.hMul, Filter.Eventually.comap
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
simp : ∀ (a b ε : G), ε > 1 → ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : G × G) ↦ p.1 * p.2

Tactic:
simp only [continuous_iff_continuousAt, Prod.forall, ContinuousAt,
      LinearOrderedCommGroup.tendsto_nhds]

Premises used: LinearOrderedCommGroup.tendsto_nhds, ContinuousAt, Prod.forall, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
inl : ∀ (δ : G) (hδ₁ : 1 < δ) (hδε : δ < ε), ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
inr : ∀ (hε_min : ∀ a < ε, a ≤ 1), ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
rcases dense_or_discrete 1 ε with ⟨δ, hδ₁, hδε⟩ | ⟨-, hε_min⟩

Premises used: OfNat.ofNat, dense_or_discrete
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
h : ∀ (a_1 : G × G), |a_1.1 / a|ₘ < δ ∧ |a_1.2 / b|ₘ < ε / δ → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]

Premises used: Iff.mpr, one_lt_div', eventually_mabs_div_lt, Filter.Eventually.prod_nhds
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
rw rw₁ : |c * d / (a * b)|ₘ = |c * d / (a * b)|ₘ
⊢ |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ

Tactic:
rw [div_mul_div_comm]

Premises used: div_mul_div_comm
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c / a * (d / b)|ₘ ≤ |c / a|ₘ * |d / b|ₘ

Tactic:
mabs_mul_le ..

Premises used: mabs_mul_le
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c / a|ₘ * |d / b|ₘ < δ * (ε / δ)

Tactic:
mul_lt_mul_of_lt_of_lt hc hd

Premises used: mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ δ * (ε / δ) = ε

Tactic:
mul_div_cancel ..

Premises used: mul_div_cancel
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
d₁ : |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ
⊢ |(c, d).1 * (c, d).2 / (a * b)|ₘ < ε

Tactic:
calc
        |c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
        _ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul_le ..
        _ < δ * (ε / δ) := mul_lt_mul_of_lt_of_lt hc hd
        _ = ε := mul_div_cancel ..

Premises used: HMul.hMul, mabs_mul_le, HDiv.hDiv, mul_div_cancel, mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
⊢ ∀ (x : G), ∀ᶠ (y : G) in 𝓝 x, y = x

Tactic:
have (x : G) : ∀ᶠ y in 𝓝 x, y = x :=
        (eventually_mabs_div_lt _ hε).mono fun y hy ↦ mabs_div_le_one.mp <| hε_min _ hy
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
this : ∀ (x : G), ∀ᶠ (y : G) in 𝓝 x, y = x
h : ∀ (a_1 : G × G), a_1.1 = a ∧ a_1.2 = b → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
filter_upwards [(this _).prod_nhds (this _)]

Premises used: Filter.Eventually.prod_nhds
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
this : ∀ (x : G), ∀ᶠ (y : G) in 𝓝 x, y = x
⊢ ∀ (a_1 : G × G), a_1.1 = a ∧ a_1.2 = b → |a_1.1 * a_1.2 / (a * b)|ₘ < ε

Tactic:
simp [hε]
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a ε : G
ε0 : ε > 1
x : G
hx : |x / a|ₘ < ε
rwa : |a / x|ₘ < ε
rwa₁ rwa₂ rwa₃ rwa₄ : |x / a|ₘ < ε
⊢ |x⁻¹ / (fun (a : G) ↦ a⁻¹) a|ₘ < ε

Tactic:
rwa [inv_div_inv, mabs_div_comm]

Premises used: mabs_div_comm, inv_div_inv
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
⊢ Continuous[inst, inst] mabs

Tactic:
continuous_id.max continuous_inv

Premises used: continuous_id, Continuous.max, ContinuousInv.continuous_inv, mabs
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
α : Type u_2
l : Filter α
f : α → G
a : G
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ |f x|ₘ) l (𝓝 |a|ₘ)

Tactic:
(continuous_mabs.tendsto _).comp h

Premises used: continuous_mabs, Continuous.tendsto, Filter.Tendsto.comp, mabs
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
⊢ Eq.{u_1 + 1} (α := Filter G) (comap mabs (𝓝 1)) (𝓝 1)

Tactic:
simp [nhds_eq_iInf_mabs_div]

Premises used: nhds_eq_iInf_mabs_div
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
α : Type u_2
l : Filter α
f : α → G
rw : Tendsto f l (𝓝 1) ↔ Tendsto f l (comap mabs (𝓝 1))
rw₁ rw₂ : Tendsto f l (𝓝 1) ↔ Tendsto f l (𝓝 1)
⊢ Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1)

Tactic:
rw [← tendsto_comap_iff, comap_mabs_nhds_one]

Premises used: comap_mabs_nhds_one, Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
X : Type u_2
inst_5 : TopologicalSpace X
f : X → G
h : Continuous[inst_5, inst] f
⊢ Continuous[inst_5, inst] fun (x : X) ↦ |f x|ₘ

Tactic:
continuous_mabs.comp h

Premises used: continuous_mabs, Continuous.comp, mabs
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
X : Type u_2
inst_5 : TopologicalSpace X
f : X → G
x : X
h : ContinuousAt f x
⊢ ContinuousAt.{u_2, u_1} (Y := G) (fun (x : X) ↦ |f x|ₘ) x

Tactic:
Filter.Tendsto.mabs h

Premises used: Filter.Tendsto.mabs, ContinuousAt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
X : Type u_2
inst_5 : TopologicalSpace X
f : X → G
s : Set X
x : X
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt.{u_2, u_1} (Y := G) (fun (x : X) ↦ |f x|ₘ) s x

Tactic:
Filter.Tendsto.mabs h

Premises used: Filter.Tendsto.mabs, ContinuousWithinAt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
X : Type u_2
inst_5 : TopologicalSpace X
f : X → G
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn.{u_2, u_1} (Y := G) (fun (x : X) ↦ |f x|ₘ) s

Tactic:
fun x hx => (h x hx).mabs

Premises used: ContinuousWithinAt.mabs, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
⊢ Tendsto (α := G) mabs (𝓝[≠] 1) (𝓝[>] 1)

Tactic:
(continuous_mabs.tendsto' (1 : G) 1 mabs_one).inf <|
    tendsto_principal_principal.2 fun _x => one_lt_mabs.2

Premises used: continuous_mabs, Iff.mpr, mabs_one, one_lt_mabs, nhdsWithin, Continuous.tendsto', Filter.Tendsto.inf, OfNat.ofNat, Filter.tendsto_principal_principal
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
⊢ (DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x) ↔ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩

Premises used: Function.Surjective.denseRange, Iff.intro
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
refine : ∀ (h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x), Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ (DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x) ↔ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
inr :
  ∀
    (this :
      ∀ {a : G} (h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x) (ha₀ : 1 < a),
        Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x)
    (ha₀ : a ≤ 1), Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
wlog! :
  ∀ {a : G} (h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x) (ha₀ : 1 < a),
    Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
⊢ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
wlog! ha₀ : 1 < a generalizing a
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
this :
  ∀ {a : G} (h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x) (ha₀ : 1 < a),
    Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
ha₀ : a ≤ 1
inr :
  ∀
    (this :
      ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
        Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
⊢ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x

Tactic:
simp only [← range_eq_univ, DenseRange] at *

Premises used: Set.range_eq_univ, DenseRange
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
inr :
  ∀ (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ HPow.hPow (α := G) 1 x)) (ha₀ : LE.le.{u_1} (α := G) 1 1),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ HPow.hPow (α := G) 1 x) univ
inr₁ : ∀ (hlt : a < 1), Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ

Tactic:
rcases ha₀.eq_or_lt with rfl | hlt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ HPow.hPow (α := G) 1 x)
ha₀ : LE.le.{u_1} (α := G) 1 1
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ HPow.hPow (α := G) 1 x) univ

Tactic:
simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h

Premises used: one_zpow, dense_iff_closure_eq, closure_singleton, Set.range_const
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)

Tactic:
simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)

Premises used: inv_zpow, Function.Surjective.range_comp, Function.comp_def, neg_surjective, HPow.hPow, zpow_neg
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)

Tactic:
have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
        simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
H : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)
inr : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) univ
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ

Tactic:
rw [← H]
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
H : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)
inr : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a⁻¹ ^ x)
inr₁ : 1 < a⁻¹
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) univ

Tactic:
apply this