awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ IsTopologicalGroup G
have refine : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
Tactic: refine IsTopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀_1 x₀ : G
⊢ Eq.{u + 1} (α := G → G) ((fun (x : G) ↦ x₀ * x * x₀⁻¹) ∘ fun (x : G) ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) id
have h : ∀ (x : G), ((fun (x : G) ↦ x₀ * x * x₀⁻¹) ∘ fun (x : G) ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
have hconj₁ : ∀ (x₀ : G), Eq.{u + 1} (α := Filter G) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1)) (𝓝 1)
Tactic: replace hconj : ∀ x₀ : G, map (x₀ * · * x₀⁻¹) (𝓝 1) = 𝓝 1 :=
    fun x₀ => map_eq_of_inverse (x₀⁻¹ * · * x₀⁻¹⁻¹) (by ext; simp [mul_assoc]) (hconj _) (hconj _)
Cleared hypotheses: hconj
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), Eq.{u + 1} (α := Filter G) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1)) (𝓝 1)
⊢ 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
have rw : 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1))
Tactic: rw [← hconj x₀]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
⊢ ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have rcases : ∀ (u : ℕ → Set G) (hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u) (u_anti : Antitone u),
  ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
Tactic: rcases (𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
⊢ ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have this : ∀ (ib : ℕ), True → ∃ (ia : ℕ × ℕ), (True ∧ True) ∧ ∀ x ∈ u ia.1 ×ˢ u ia.2, x.1 * x.2 ∈ u ib
Tactic: have :=
    ((hu.prod_nhds hu).tendsto_iff hu).mp
      (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), True → ∃ (ia : ℕ × ℕ), (True ∧ True) ∧ ∀ x ∈ u ia.1 ×ˢ u ia.2, x.1 * x.2 ∈ u ib
⊢ ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have this₁ : ∀ (ib : ℕ), ∃ (a : ℕ) (b : ℕ), True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
Tactic: simp only [and_self_iff, mem_prod, and_imp, Prod.forall, Prod.exists,
    forall_true_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ (a : ℕ) (b : ℕ), True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n : ℕ
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
have rcases : ∀ (j k : ℕ) (h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
Tactic: rcases this n with ⟨j, k, -, h⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ (a : ℕ) (b : ℕ), True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
have refine : ∀ (m : ℕ) (hm : m ∈ Ici (max j k)), u m * u m ⊆ u n
Tactic: refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ (a : ℕ) (b : ℕ), True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
Tactic: have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n := by
    intro n
    rcases this n with ⟨j, k, -, h⟩
    refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩
    rintro - ⟨a, ha, b, hb, rfl⟩
    exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ (a : ℕ) (b : ℕ), True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
have obtain : ∀ (φ : ℕ → ℕ) (hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)) (φ_anti_basis : HasAntitoneBasis (𝓝 1) (u ∘ φ)),
  ∃ (u : ℕ → Set G), HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
Tactic: obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)
have refine : ∀ (h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))), Tendsto f l (𝓝 c)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)
have h₁ : ∀ (k : α), f k = f k / b / b⁻¹
Tactic: convert! h.div_const' b⁻¹ with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : ∀ (k : α), f k = f k / b / b⁻¹
⊢ Tendsto f l (𝓝 c)
have h₂ : c = c / b / b⁻¹
Tactic: convert! h.div_const' b⁻¹ with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹
have h₁ : f k = f k / (b⁻¹ * b)
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
h₁ : f k = f k / (b⁻¹ * b)
⊢ f k = f k / b / b⁻¹
have h₂ : f k = f k / 1
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
h₁ : f k = f k / (b⁻¹ * b)
h₂ : f k = f k / 1
⊢ f k = f k / b / b⁻¹
have h₃ : f k = f k
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹
have h₁ : c = c / (b⁻¹ * b)
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : c = c / (b⁻¹ * b)
⊢ c = c / b / b⁻¹
have h₂ : c = c / 1
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : GroupWithZero G
inst_1 : TopologicalSpace G
inst_2 : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : c = c / (b⁻¹ * b)
h₂ : c = c / 1
⊢ c = c / b / b⁻¹
have h₃ : c = c
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)
have refine : ∀ (h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))), Tendsto f l (𝓝 c)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)
have h₁ : ∀ (k : α), f k = f k / b / b⁻¹
Tactic: convert! h.div_const' b⁻¹ with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : ∀ (k : α), f k = f k / b / b⁻¹
⊢ Tendsto f l (𝓝 c)
have h₂ : c = c / b / b⁻¹
Tactic: convert! h.div_const' b⁻¹ with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹
have h₁ : f k = f k / (b⁻¹ * b)
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
h₁ : f k = f k / (b⁻¹ * b)
⊢ f k = f k / b / b⁻¹
have h₂ : f k = f k / 1
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
k : α
h₁ : f k = f k / (b⁻¹ * b)
h₂ : f k = f k / 1
⊢ f k = f k / b / b⁻¹
have h₃ : f k = f k
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹
have h₁ : c = c / (b⁻¹ * b)
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : c = c / (b⁻¹ * b)
⊢ c = c / b / b⁻¹
have h₂ : c = c / 1
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
α : Type u
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))
h₁ : c = c / (b⁻¹ * b)
h₂ : c = c / 1
⊢ c = c / b / b⁻¹
have h₃ : c = c
Tactic: rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)
have refine : ∀ (h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))), Tendsto f l (𝓝 c)
Tactic: refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
⊢ Tendsto f l (𝓝 c)
have h₁ : ∀ (k : α), f k = (b / f k)⁻¹ * b
Tactic: convert! h.inv.mul_const b with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
h₁ : ∀ (k : α), f k = (b / f k)⁻¹ * b
⊢ Tendsto f l (𝓝 c)
have h₂ : c = (b / c)⁻¹ * b
Tactic: convert! h.inv.mul_const b with k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
k : α
⊢ f k = (b / f k)⁻¹ * b
have h₁ : f k = f k / b * b
Tactic: rw [inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
k : α
h₁ : f k = f k / b * b
⊢ f k = (b / f k)⁻¹ * b
have h₂ : f k = f k
Tactic: rw [inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
⊢ c = (b / c)⁻¹ * b
have h₁ : c = c / b * b
Tactic: rw [inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))
h₁ : c = c / b * b
⊢ c = (b / c)⁻¹ * b
have h₂ : c = c
Tactic: rw [inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite.{w} (α := ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ
Tactic: have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ
⊢ Set.Finite.{w} (α := ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have H₁ : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
Tactic: rw [preimage_compl, compl_compl] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
⊢ Set.Finite.{w} (α := ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have h : Eq (α := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
  (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
Tactic: convert! H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
⊢ Eq (α := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
have h : ∀ (x : ↥S),
  Membership.mem (γ := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty} x ↔
    Membership.mem (γ := Set ↥S)
      (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (α := ↥S) (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K))
x : ↥S
⊢ Membership.mem (γ := Set ↥S) {γ : ↥S | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty} x ↔
    Membership.mem (γ := Set ↥S)
      (preimage (β := G) (⇑S.subtype : (a : ↥S) → G) ((fun (p : G × G) ↦ p.1 / p.2) '' L ×ˢ K)) x
have h : (x • K ∩ L).Nonempty ↔ ∃ (a : G) (b : G), (a, b) ∈ L ×ˢ K ∧ a / b = (↑x : G)
Tactic: simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite.{w} (α := ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
Tactic: have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prodMap continuous_id
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
⊢ Set.Finite.{w} (α := ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have H : Set.Finite (α := ↥S)
  (preimage (β := G) (⇑S.subtype : (a : ↥S) → G)
      (((fun (p : G × G) ↦ p.1 * p.2) ∘ fun (p : G × G) ↦ (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ
Tactic: have H : Set.Finite _ :=
        hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H :
  Set.Finite (α := ↥S)
    (preimage (β := G) (⇑S.subtype : (a : ↥S) → G)
        (((fun (p : G × G) ↦ p.1 * p.2) ∘ fun (p : G × G) ↦ (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ
⊢ Set.Finite.{w} (α := ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have H₁ : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
Tactic: simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (α := ↥S) (⇑S.subtype : (a : ↥S) → G) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : G × G) ↦ (p.1⁻¹, p.2)
H : Set.Finite (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹' (fun (a : G × G) ↦ a.1⁻¹ * a.2) '' K ×ˢ L)
⊢ Set.Finite.{w} (α := ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty}
have apply : Set.Finite (α := ↥S)
  (preimage (β := ↥S.op) (⇑S.equivOp : (a : ↥S) → ↥S.op) {γ : ↥S.op | ((fun (x : G) ↦ γ • x) '' K ∩ L).Nonempty})
Tactic: apply Finite.of_preimage _ (equivOp S).surjective