awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ Eq.{u + 1} (α := Filter G) (map (α := G) ((fun (x : G) ↦ x * x₀⁻¹) ∘ fun (x : G) ↦ x * x₀) (𝓝 1)) (𝓝 1)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
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

Tactic:
IsTopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => ?_

Premises used: IsTopologicalGroup.of_nhds_one'
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)
refine : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
⊢ IsTopologicalGroup G

Tactic:
refine IsTopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => ?_

Premises used: IsTopologicalGroup.of_nhds_one'
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h : ∀ (x : G), ((fun (x : G) ↦ x₀ * x * x₀⁻¹) ∘ fun (x : G) ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) x = id x
⊢ Eq.{u + 1} (α := G → G) ((fun (x : G) ↦ x₀ * x * x₀⁻¹) ∘ fun (x : G) ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) id

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Group.Basic
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₀ x : G
⊢ ((fun (x : G) ↦ x₀ * x * x₀⁻¹) ∘ fun (x : G) ↦ x₀⁻¹ * x * x₀⁻¹⁻¹) x = id x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.Group.Basic
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₀ : 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 _)
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)
rw : 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1))
⊢ 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)

Tactic:
rw [← hconj x₀]
-- Module: Mathlib.Topology.Algebra.Group.Basic
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₀) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1))

Tactic:
simpa [Function.comp_def] using hleft _

Premises used: Function.comp_def
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type u
inst : CommGroup 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), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
simpa using tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
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
⊢ ∃ (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⟩

Premises used: nhds, Filter.exists_antitone_basis, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
⊢ Tendsto (β := G) (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (1, 1)) (𝓝 1)

Tactic:
simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G)

Premises used: continuous_mul, Prod.mk, Continuous.tendsto, mul_one, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
⊢ ∀ (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))
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
⊢ ∀ (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

Premises used: forall_true_left, and_imp, Set.mem_prod, Prod.forall, and_self_iff, Prod.exists
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 : ℕ
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
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n

Tactic:
rcases this n with ⟨j, k, -, h⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
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

Tactic:
atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩

Premises used: Iff.mpr, Filter.atTop_basis, Max.max, And.intro, Exists.intro, Filter.HasBasis.eventually_iff, True.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
refine : ∀ (m : ℕ) (hm : m ∈ Ici (max j k)), u m * u m ⊆ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n

Tactic:
refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩

Premises used: Iff.mpr, Filter.atTop_basis, Max.max, And.intro, Exists.intro, Filter.HasBasis.eventually_iff, True.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 : ℕ
hm : m ∈ Ici (max j k)
a : G
ha : a ∈ u m
b : G
hb : b ∈ u m
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ u n

Tactic:
h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)

Premises used: le_max_right, Set.Mem, LE.le.trans, le_max_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 : ℕ
hm : m ∈ Ici (max j k)
a : G
ha : a ∈ u m
b : G
hb : b ∈ u m
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ u n

Tactic:
exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
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

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)
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
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
⊢ ∃ (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

Premises used: Filter.HasAntitoneBasis.mk, Filter.HasAntitoneBasis.subbasis_with_rel
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
φ : ℕ → ℕ
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:
⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩

Premises used: Function.comp, Nat.lt_succ_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
φ : ℕ → ℕ
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:
exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
c : G
f : α → G
l : Filter α
h : Tendsto f l (𝓝 c)
b : G
⊢ Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))

Tactic:
h.div' tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.div'
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)

Tactic:
⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩

Premises used: Filter.Tendsto.div_const', Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 α
refine : ∀ (h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))), Tendsto f l (𝓝 c)
⊢ 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⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 (fun (x : α) ↦ f x / b / b⁻¹) l (𝓝 (c / b / b⁻¹))

Tactic:
h.div_const' b⁻¹

Premises used: Filter.Tendsto.div_const', Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
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⁻¹
h₂ : c = c / b / b⁻¹
⊢ Tendsto f l (𝓝 c)

Tactic:
convert! h.div_const' b⁻¹ with k

Premises used: Filter.Tendsto.div_const', Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₃ h₄ : f k = f k
⊢ f k = f k / b / b⁻¹

Tactic:
rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]

Premises used: div_mul_eq_div_div_swap, div_one, inv_mul_cancel₀
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₃ h₄ : c = c
⊢ c = c / b / b⁻¹

Tactic:
rw [← div_mul_eq_div_div_swap, inv_mul_cancel₀ hb, div_one]

Premises used: div_mul_eq_div_div_swap, div_one, inv_mul_cancel₀
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)

Tactic:
⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩

Premises used: Filter.Tendsto.div_const', Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 α
refine : ∀ (h : Tendsto (fun (x : α) ↦ f x / b) l (𝓝 (c / b))), Tendsto f l (𝓝 c)
⊢ 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⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 (fun (x : α) ↦ f x / b / b⁻¹) l (𝓝 (c / b / b⁻¹))

Tactic:
h.div_const' b⁻¹

Premises used: Filter.Tendsto.div_const', Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
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⁻¹
h₂ : c = c / b / b⁻¹
⊢ Tendsto f l (𝓝 c)

Tactic:
convert! h.div_const' b⁻¹ with k

Premises used: Filter.Tendsto.div_const', Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₃ h₄ : f k = f k
⊢ f k = f k / b / b⁻¹

Tactic:
rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]

Premises used: inv_mul_cancel, div_mul_eq_div_div_swap, div_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₃ h₄ : c = c
⊢ c = c / b / b⁻¹

Tactic:
rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]

Premises used: inv_mul_cancel, div_mul_eq_div_div_swap, div_one
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto f l (𝓝 c)
⊢ Tendsto (fun (x : α) ↦ b / f x) l (𝓝 (b / c))

Tactic:
tendsto_const_nhds.div' h

Premises used: tendsto_const_nhds, Filter.Tendsto.div'
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
a : G
⊢ Continuous[inst, inst] fun (x : G) ↦ a / x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
a : G
⊢ Continuous[inst, inst] fun (x : G) ↦ x / a

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
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)

Tactic:
⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩

Premises used: Filter.Tendsto.const_div', Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
α : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
refine : ∀ (h : Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c))), Tendsto f l (𝓝 c)
⊢ Tendsto (fun (k : α) ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩
-- Module: Mathlib.Topology.Algebra.Group.Basic
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 (fun (x : α) ↦ (b / f x)⁻¹ * b) l (𝓝 ((b / c)⁻¹ * b))

Tactic:
h.inv.mul_const b

Premises used: Filter.Tendsto.inv, Filter.Tendsto.mul_const
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₂ : c = (b / c)⁻¹ * b
⊢ Tendsto f l (𝓝 c)

Tactic:
convert! h.inv.mul_const b with k

Premises used: Filter.Tendsto.inv, Filter.Tendsto.mul_const
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₂ h₃ : f k = f k
⊢ f k = (b / f k)⁻¹ * b

Tactic:
rw [inv_div, div_mul_cancel]

Premises used: inv_div, div_mul_cancel
-- Module: Mathlib.Topology.Algebra.Group.Basic
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
h₂ h₃ : c = c
⊢ c = (b / c)⁻¹ * b

Tactic:
rw [inv_div, div_mul_cancel]

Premises used: inv_div, div_mul_cancel
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
a : G
⊢ IsOpenMap (Y := G) fun (x : G) ↦ a / x

Tactic:
(Homeomorph.divLeft _).isOpenMap

Premises used: Homeomorph.divLeft, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
a : G
⊢ IsClosedMap (Y := G) fun (x : G) ↦ a / x

Tactic:
(Homeomorph.divLeft _).isClosedMap

Premises used: Homeomorph.divLeft, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
a : G
⊢ IsOpenMap (Y := G) fun (x : G) ↦ x / a

Tactic:
(Homeomorph.divRight a).isOpenMap

Premises used: Homeomorph.divRight, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
a : G
⊢ IsClosedMap (Y := G) fun (x : G) ↦ x / a

Tactic:
(Homeomorph.divRight a).isClosedMap

Premises used: Homeomorph.divRight, Homeomorph.isClosedMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun (x_1 : α) ↦ x) l (𝓝 x)
h : Tendsto.{u_1, w} (β := G) (fun (x_1 : α) ↦ u x_1 / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)

Tactic:
simpa using h.mul A

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun (x_1 : α) ↦ x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto.{u_1, w} (β := G) (fun (x_1 : α) ↦ u x_1 / x) l (𝓝 1)

Tactic:
simpa using h.div' A

Premises used: Filter.Tendsto.div'
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : G
⊢ comap (β := G) (fun (x_1 : G) ↦ x_1 / x) (𝓝 1) = 𝓝 x

Tactic:
simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

Premises used: nhds_translation_mul_inv, div_eq_mul_inv