awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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)
⊢ LocallyCompactSpace.{u_5} (PontryaginDual H)
have refine_1 : ∀ {n : ℕ} {x : Circle}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)
Tactic: refine ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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_1 : ∀ {n : ℕ} {x : Circle}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)
⊢ LocallyCompactSpace.{u_5} (PontryaginDual H)
have refine_2 : Filter.HasBasis (nhds 1) (fun (x : ℕ) ↦ True) Vn
Tactic: refine ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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 ∈ Vn n
h2 : x * x ∈ Vn n
⊢ x ∈ Vn (n + 1)
have refine_1 : ∀ (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 / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
Tactic: rw [hVn] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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 / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
have refine_1 : ∀ (h2 : |((↑x : ℂ) * (↑x : ℂ)).arg| < Real.pi / HPow.hPow (α := ℝ) 2 (n + 1)),
  (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioc (-Real.pi) Real.pi
Tactic: rwa [Circle.coe_mul, Complex.arg_mul x.coe_ne_zero x.coe_ne_zero,
      ← two_mul, abs_mul, abs_two, ← lt_div_iff₀' two_pos, div_div, ← pow_succ] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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 + (↑x : ℂ).arg ∈ Set.Ioc (-Real.pi) Real.pi
have refine_1 : (↑x : ℂ).arg + (↑x : ℂ).arg ∈ Set.Ioo (-Real.pi) Real.pi
Tactic: apply Set.Ioo_subset_Ioc_self
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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 + (↑x : ℂ).arg ∈ Set.Ioo (-Real.pi) Real.pi
have refine_1 : |(↑x : ℂ).arg| < Real.pi / 2
Tactic: rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos]
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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
have refine_1 : Real.pi / HPow.hPow (α := ℝ) 2 (n + 1) ≤ Real.pi / 2
Tactic: refine h1.trans_le ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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)
⊢ Real.pi / HPow.hPow (α := ℝ) 2 (n + 1) ≤ Real.pi / 2
have refine_1 : 2 ≤ HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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)
⊢ Filter.HasBasis (nhds 1) (fun (x : ℕ) ↦ True) Vn
have refine_2 : Filter.HasBasis (Filter.map (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) (nhds 0)) (fun (x : ℕ) ↦ True) Vn
Tactic: rw [← Circle.exp_zero, ← isLocalHomeomorph_circleExp.map_nhds_eq 0]
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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)
⊢ Filter.HasBasis (Filter.map (α := ℝ) (⇑Circle.exp : (a : ℝ) → Circle) (nhds 0)) (fun (x : ℕ) ↦ True) Vn
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (hypothesis)
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
⊢ Membership.mem (γ := Set ℝ) {b : ℝ | |b| < x} t
have ht₁ : |t| < Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
Tactic: rw [Set.mem_setOf_eq] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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
have refine_2 : Real.pi / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1) ≤ x
Tactic: refine lt_of_lt_of_le ht ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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 / HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1) ≤ x
have refine_2 : Real.pi / x ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
Tactic: rw [div_le_iff₀' (pow_pos two_pos _), ← div_le_iff₀ hx]
-- Lean 4 proof step from Mathlib.Topology.Algebra.PontryaginDual (goal)
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)
have refine_2 : (↑⌈Real.pi / x⌉₊ : ℝ) ≤ HPow.hPow (α := ℝ) 2 (⌈Real.pi / x⌉₊ + 1)
Tactic: refine (Nat.le_ceil (Real.pi / x)).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
have 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)
Tactic: refine ⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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)
⊢ 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)
have 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
Tactic: refine ⟨fun h ↦ ⟨inferInstance, fun 𝒰 x₁ x₂ h' ↦ ?_⟩, fun ⟨cont, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
have 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)
Tactic: rw [properSMul_iff, isProperMap_iff_ultrafilter] at h
Cleared hypotheses: h, 𝒰, x₁, x₂, h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
⊢ ∃ (g : G), g • x₂ = x₁ ∧ Tendsto fst (↑𝒰 : Filter (G × X)) (𝓝 g)
have 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)
Tactic: rcases h.2 h' with ⟨gx, hgx1, hgx2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
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)
have refine_1 : gx.1 • x₂ = x₁
Tactic: refine ⟨gx.1, ?_, (continuous_fst.tendsto gx).mono_left hgx2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
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₂))
gx : G × X
hgx1 : (gx.1 • gx.2, gx.2) = (x₁, x₂)
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
⊢ gx.1 • x₂ = x₁
have hgx1₁ : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
Tactic: simp only [Prod.mk.injEq] at hgx1
Cleared hypotheses: hgx1
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
gx : G × X
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
⊢ gx.1 • x₂ = x₁
have refine_1 : gx.1 • gx.2 = x₁
Tactic: rw [← hgx1.2, hgx1.1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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₂))
gx : G × X
hgx2 : (↑𝒰 : Filter (G × X)) ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
refine_1 : gx.1 • gx.2 = x₁
⊢ gx.1 • x₂ = x₁
have refine_1₁ : x₁ = x₁
Tactic: rw [← hgx1.2, hgx1.1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_1 :
  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
have refine_2 : (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
Tactic: rw [properSMul_iff, isProperMap_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
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_1 :
  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)
⊢ (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
have refine_2 : ∀ (𝒰 : Ultrafilter (G × X)) (x : X × X) (x₁ x₂ : X)
  (hxx : Tendsto (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) (↑𝒰 : Filter (G × X)) (𝓝 (x₁, x₂))),
  ∃ (x : G × X), (x.1 • x.2, x.2) = (x₁, x₂) ∧ (↑𝒰 : Filter (G × X)) ≤ 𝓝 x
Tactic: refine ⟨by fun_prop, fun 𝒰 (x₁, x₂) hxx ↦ ?_⟩