awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 : (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioo (-Real.pi) Real.pi
⊢ (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioc (-Real.pi) Real.pi

Tactic:
apply Set.Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 : |(↑x : ℂ).arg| < Real.pi / 2
⊢ (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioo (-Real.pi) Real.pi

Tactic:
rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos]

Premises used: Set.mem_Ioo, lt_div_iff₀', abs_mul, two_mul, abs_lt, abs_two
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ |(↑x : ℂ).arg| < Real.pi / 2

Tactic:
h1.trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 : Real.pi / HPow.hPow (α := ℝ) 2 (n + 1) ≤ Real.pi / 2
⊢ |(↑x : ℂ).arg| < Real.pi / 2

Tactic:
refine h1.trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_1 : 2 ≤ HPow.hPow (α := ℝ) 2 (n + 1)
⊢ Real.pi / HPow.hPow (α := ℝ) 2 (n + 1) ≤ Real.pi / 2

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ 2 ≤ HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
le_self_pow₀ one_le_two n.succ_ne_zero

Premises used: Nat.succ_ne_zero, le_self_pow₀, one_le_two
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
n : ℕ
x : Circle
h1 : |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ 2 ≤ HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
exact le_self_pow₀ one_le_two n.succ_ne_zero

Premises used: Nat.succ_ne_zero, le_self_pow₀
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_2 : Filter.HasBasis (Filter.map (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) (nhds 0)) (fun (x : ℕ) ↦ True) Vn
⊢ Filter.HasBasis (nhds 1) (fun (x : ℕ) ↦ True) Vn

Tactic:
rw [← Circle.exp_zero, ← isLocalHomeomorph_circleExp.map_nhds_eq 0]

Premises used: Circle.exp_zero, IsLocalHomeomorph.map_nhds_eq, isLocalHomeomorph_circleExp, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
k : ℕ
h : True
⊢ 0 < Real.pi / HPow.hPow (α := ℝ) 2 (k + 1)

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
refine_2 :
  ∀ (x : ℝ) (hx : 0 < x) (t : ℝ)
    (ht : Membership.mem (γ := Set ℝ) {b : ℝ | |b| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)} t),
    Membership.mem (γ := Set ℝ) {b : ℝ | |b| < x} t
⊢ Filter.HasBasis (Filter.map (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) (nhds 0)) (fun (x : ℕ) ↦ True) Vn

Tactic:
refine ((nhds_basis_zero_abs_lt ℝ).to_hasBasis
        (fun x hx ↦ ⟨Nat.ceil (Real.pi / x), trivial, fun t ht ↦ ?_⟩)
          fun k _ ↦ ⟨Real.pi / 2 ^ (k + 1), by positivity, le_rfl⟩).map Circle.exp

Premises used: Real, Real.pi, le_rfl, nhds_basis_zero_abs_lt, HDiv.hDiv, Filter.HasBasis.map, Circle.exp, HPow.hPow, HAdd.hAdd, Nat.ceil, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : Membership.mem (γ := Set ℝ) {b : ℝ | |b| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)} t
⊢ |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)

Tactic:
rw [Set.mem_setOf_eq] at ht ⊢

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
⊢ |t| < x

Tactic:
lt_of_lt_of_le ht ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
refine_2 : Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1) ≤ x
⊢ |t| < x

Tactic:
refine lt_of_lt_of_le ht ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
refine_2 : Real.pi / x ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
⊢ Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1) ≤ x

Tactic:
rw [div_le_iff₀' (pow_pos two_pos _), ← div_le_iff₀ hx]

Premises used: div_le_iff₀, pow_pos, div_le_iff₀'
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
⊢ Real.pi / x ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)

Tactic:
(Nat.le_ceil (Real.pi / x)).trans ?_

Premises used: Real.pi, HDiv.hDiv, Nat.le_ceil, LE.le.trans
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
refine_2 : (↑⌈Real.pi / x⌉₊ : ℝ) ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
⊢ Real.pi / x ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)

Tactic:
refine (Nat.le_ceil (Real.pi / x)).trans ?_

Premises used: Real.pi, HDiv.hDiv, Nat.le_ceil, LE.le.trans
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : CommGroup G
inst_4 : Group H
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalGroup G
inst_11 : IsTopologicalGroup H
inst_12 : LocallyCompactSpace H
Vn : ℕ → Set Circle :=
  fun (n : ℕ) ↦
    Set.image (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) {x : ℝ | |x| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)}
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x : ℂ).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)
x : ℝ
hx : 0 < x
t : ℝ
ht : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
⊢ (↑⌈Real.pi / x⌉₊ : ℝ) ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)

Tactic:
exact_mod_cast (Nat.le_succ _).trans Nat.lt_two_pow_self.le

Premises used: LT.lt.le, Nat.le_succ, Nat.lt_two_pow_self, LE.le.trans
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
f : A →ₜ* B
x : PontryaginDual B
y : A
⊢ Eq (α := Circle)
    ((((map f : (a : PontryaginDual B) → PontryaginDual A) x : PontryaginDual A) : (a : A) → Circle) y : Circle)
    ((x : (a : B) → Circle) ((f : (a : A) → B) y) : Circle)

Tactic:
rfl

Premises used: PontryaginDual, ContinuousMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
⊢ Eq (α := ContinuousMonoidHom.{u_2, u_1} (PontryaginDual B) (PontryaginDual A)) (map 1) 1

Tactic:
ext fun x => ext (fun _y => OneHomClass.map_one x)

Premises used: OneHomClass.map_one, ContinuousMonoidHom.ext
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
g : B →ₜ* C
f : A →ₜ* B
⊢ map (g.comp f) = (map f).comp (map g)

Tactic:
ext fun _x => ext fun _y => rfl

Premises used: ContinuousMonoidHom.ext, rfl
-- Module: Mathlib.Topology.Algebra.PontryaginDual
Goal:
A : Type u_1
G : Type u_4
inst : Monoid A
inst_1 : CommGroup G
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
f g : A →ₜ* G
⊢ map (f * g) = map f * map g

Tactic:
ext fun x => ext fun y => map_mul x (f y) (g y)

Premises used: map_mul, ContinuousMonoidHom.ext, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.ProperAction.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : AddTorsor V P
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
x : V × P
⊢ (fun (pq : P × P) ↦ (pq.1 -ᵥ pq.2, pq.2)) ((fun (vp : V × P) ↦ (vp.1 +ᵥ vp.2, vp.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : AddTorsor V P
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
x : P × P
⊢ (fun (vp : V × P) ↦ (vp.1 +ᵥ vp.2, vp.2)) ((fun (pq : P × P) ↦ (pq.1 -ᵥ pq.2, pq.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : AddTorsor V P
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
Φ : V × P ≃ₜ P × P :=
  { toFun := fun (vp : V × P) ↦ (vp.1 +ᵥ vp.2, vp.2), invFun := fun (pq : P × P) ↦ (pq.1 -ᵥ pq.2, pq.2), left_inv := ⋯,
    right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := P × P) fun (gx : V × P) ↦ (gx.1 +ᵥ gx.2, gx.2)

Tactic:
Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : AddTorsor V P
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
Φ : V × P ≃ₜ P × P :=
  { toFun := fun (vp : V × P) ↦ (vp.1 +ᵥ vp.2, vp.2), invFun := fun (pq : P × P) ↦ (pq.1 -ᵥ pq.2, pq.2), left_inv := ⋯,
    right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := P × P) fun (gx : V × P) ↦ (gx.1 +ᵥ gx.2, gx.2)

Tactic:
exact Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
⊢ ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩

Premises used: inferInstance, And.intro, Iff.intro, _private.0.properSMul_iff_continuousSMul_ultrafilter_tendsto.match_1, ProperSMul
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
refine_1 :
  ∀ (h : ProperSMul G X) (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X)
    (h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))),
    ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
refine_2 :
  (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)) →
    ∀ (cont : ContinuousSMul G X)
      (h :
        ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
          Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
            ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)),
      ProperSMul G X
⊢ ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂)) →
          ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h : ProperSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
refine_1 :
  ∀
    (h :
      (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
        ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
          Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
            ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x)
    (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X)
    (h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))),
    ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
rw [properSMul_iff, isProperMap_iff_ultrafilter] at h

Premises used: properSMul_iff, isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 y) →
        ∃ (x : G × X), (x.1 • x.2, x.2) = y ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))
refine_1 :
  ∀ (gx : G × X) (hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)) (hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx),
    ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)

Tactic:
rcases h.2 h' with ⟨gx, hgx1, hgx2⟩

Premises used: And.right