awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have inr : ∀ (hc : c < 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Tactic: rcases lt_trichotomy c 0 with (hc | rfl | hc)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
inr : ∀ (hc : c < 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have inr₁ : Tendsto (fun (x : 𝕜) ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (Eq.{u_1 + 1} (α := 𝕜) 0 0 ∨ n = 0) ∧ 0 = d
Tactic: rcases lt_trichotomy c 0 with (hc | rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
inr : ∀ (hc : c < 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
inr₁ : Tendsto (fun (x : 𝕜) ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (Eq.{u_1 + 1} (α := 𝕜) 0 0 ∨ n = 0) ∧ 0 = d
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have inr₂ : ∀ (hc : 0 < c), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Tactic: rcases lt_trichotomy c 0 with (hc | rfl | hc)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atBot
Tactic: have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
have this : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ c * x ^ n) atTop atTop
Tactic: have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
have refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)), n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
refine_1 : ∀ (h : Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)), n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
have refine_2 : ∀ (h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0
have refine_1 : Int.ofNat n = 0 ∧ c = d
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (hypothesis)
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)
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
have hn : Int.negSucc n < 0
Tactic: have hn := Int.negSucc_lt_zero n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
have 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
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)⟩
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
have 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
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)⟩
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
have refine_2 : ∀ (h : n = 0 ∧ c = d), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
⊢ Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
have refine_2₁ : ∀ (h : n < 0 ∧ d = 0), Tendsto (fun (x : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 : 𝕜) ↦ c * x ^ n) atTop (𝓝 d)
have refine_2 : Tendsto (fun (x : 𝕜) ↦ d) atTop (𝓝 d)
Tactic: simp only [h.left, h.right, zpow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have rw : Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0)) (𝓝 0 ⊓ 𝓟 (Ioi 0))
Tactic: rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi₀ _ hx, zero_div]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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) ⊓ 𝓟 (Ioi 0)) (𝓝 0 ⊓ 𝓟 (Ioi 0))
have e_a : Eq.{u_1 + 1} (α := Filter 𝕜) (comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝 0)) (𝓝 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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)
have e_a : Eq (α := Filter 𝕜) (𝓝 ((Homeomorph.symm (Homeomorph.mulLeft₀ x sorry) : (a : 𝕜) → 𝕜) 0) : Filter 𝕜) (𝓝 0 : Filter 𝕜)
Tactic: refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
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 𝓝[>] 0, p (x * ε)
have rw : ∀ᶠ (ε : 𝕜) in comap (β := 𝕜) (fun (x_1 : 𝕜) ↦ x * x_1) (𝓝[>] 0), p (x * ε)
Tactic: rw [← comap_mulLeft_nhdsGT_zero hx]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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[instTopologicalSpaceProd, inst] fun (p : G × G) ↦ p.1 * p.2
have simp : ∀ (a b ε : G), ε > 1 → ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
Tactic: simp only [continuous_iff_continuousAt, Prod.forall, ContinuousAt,
      LinearOrderedCommGroup.tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
have inl : ∀ (δ : G) (hδ₁ : 1 < δ) (hδε : δ < ε), ∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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)|ₘ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
have inr : ∀ (hε_min : ∀ a < ε, a ≤ 1), ∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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δε : δ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
have h : ∀ (a_1 : G × G), |a_1.1 / a|ₘ < δ ∧ |a_1.2 / b|ₘ < ε / δ → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
Tactic: filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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 * d / (a * b)|ₘ = |c / a * (d / b)|ₘ
have rw : |c * d / (a * b)|ₘ = |c * d / (a * b)|ₘ
Tactic: rw [div_mul_div_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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, d).1 * (c, d).2 / (a * b)|ₘ < ε
have d₁ : |c * d / (a * b)|ₘ = |c / a * (d / 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 ..
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (hypothesis)
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
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
have h : ∀ (a_1 : G × G), a_1.1 = a ∧ a_1.2 = b → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
Tactic: filter_upwards [(this _).prod_nhds (this _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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|ₘ < ε
⊢ |x⁻¹ / (fun (a : G) ↦ a⁻¹) a|ₘ < ε
have rwa : |a / x|ₘ < ε
Tactic: rwa [inv_div_inv, mabs_div_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1)
have rw : Tendsto f l (𝓝 1) ↔ Tendsto f l (comap mabs (𝓝 1))
Tactic: rw [← tendsto_comap_iff, comap_mabs_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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))
⊢ Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1)
have rw₁ : Tendsto f l (𝓝 1) ↔ Tendsto f l (𝓝 1)
Tactic: rw [← tendsto_comap_iff, comap_mabs_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
have refine : ∀ (h : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
have 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
Tactic: wlog! ha₀ : 1 < a generalizing a
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
have 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
Tactic: wlog! ha₀ : 1 < a generalizing a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Surjective.{1, u_1 + 1} (β := G) fun (x : ℤ) ↦ a ^ x
have 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
Tactic: simp only [← range_eq_univ, DenseRange] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
have 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
Tactic: rcases ha₀.eq_or_lt with rfl | hlt
Cleared hypotheses: a, h, ha₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
have inr₁ : ∀ (hlt : a < 1), Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
Tactic: rcases ha₀.eq_or_lt with rfl | hlt
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (hypothesis)
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) univ
have H : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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)
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
have inr : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) univ
Tactic: rw [← H]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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)
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) univ
have inr : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a⁻¹ ^ x)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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)
⊢ Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) univ
have inr₁ : 1 < a⁻¹
Tactic: apply this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (hypothesis)
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
ha₀ : 1 < a
b : G
⊢ ∃ (m : ℤ), a ^ m ∈ Ioo b (b * a * a)
have hne : (Ioo b (b * a * a)).Nonempty
Tactic: have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
ha₀ : 1 < a
b : G
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have obtain : ∀ (m : ℤ) (hm : b < a ^ m) (hm' : a ^ m < b * a * a), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
Tactic: obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have inl : ∀ (hm : a ^ (m - 1) < a ^ m) (hm' : a ^ m < a ^ (m - 1) * a * a), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = a ^ (m - 1)
Tactic: rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne
Cleared hypotheses: b, hm, hm'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
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
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
inl :
  ∀ (hm : a ^ (m - 1) < a ^ m) (hm' : a ^ m < a ^ (m - 1) * a * a), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = a ^ (m - 1)
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have inr : ∀ (hne : b ≠ a ^ (m - 1)), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
Tactic: rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne