awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
H : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)
⊢ Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a⁻¹ ^ x)

Tactic:
simpa only [H, one_lt_inv']

Premises used: one_lt_inv'
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)
ha₀ : a ≤ 1
this :
  ∀ {a : G} (h : Dense.{u_1} (X := G) (range fun (x : ℤ) ↦ a ^ x)) (ha₀ : 1 < a),
    Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a ^ x) univ
hlt : a < 1
H : Eq.{u_1 + 1} (α := Set G) (range fun (x : ℤ) ↦ a⁻¹ ^ x) (range fun (x : ℤ) ↦ a ^ x)
⊢ 1 < a⁻¹

Tactic:
simpa only [H, one_lt_inv']

Premises used: one_lt_inv'
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ b * a ∈ Ioo b (b * a * a)

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ (Ioo b (b * a * a)).Nonempty

Tactic:
have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
hne : (Ioo b (b * a * a)).Nonempty
⊢ ∃ (m : ℤ), a ^ m ∈ Ioo b (b * a * a)

Tactic:
simpa using h.exists_mem_open isOpen_Ioo hne

Premises used: isOpen_Ioo, DenseRange.exists_mem_open
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
obtain : ∀ (m : ℤ) (hm : b < a ^ m) (hm' : a ^ m < b * a * a), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b

Tactic:
obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne

Premises used: HMul.hMul, Set.Ioo
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
inl :
  ∀ (hm : a ^ (m - 1) < a ^ m) (hm' : a ^ m < a ^ (m - 1) * a * a), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = a ^ (m - 1)
inr : ∀ (hne : b ≠ a ^ (m - 1)), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b

Tactic:
rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne

Premises used: HSub.hSub, HPow.hPow, eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
m : ℤ
hm : a ^ (m - 1) < a ^ m
hm' : a ^ m < a ^ (m - 1) * a * a
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = a ^ (m - 1)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
rcases : ∀ (l : ℤ) (hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b

Tactic:
rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩

Premises used: isOpen_Ioo, DenseRange.exists_mem_open
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ m < l ∧ l < m + 1

Tactic:
simpa [zpow_lt_zpow_iff_right ha₀] using hl

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ m < l ∧ l < m + 1

Tactic:
have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this_1 : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
this : m < l ∧ l < m + 1
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
inr : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b

Tactic:
suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty by
    rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
    have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
    lia
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
inr : ∀ (hlt : b < a ^ (m - 1)), (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
inr₁ : ∀ (hlt : a ^ (m - 1) < b), (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
rcases hne.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
⟨b * a * a, hm', ?_⟩

Premises used: HMul.hMul, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
inr : b * a * a < a ^ (m + 1)
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
refine ⟨b * a * a, hm', ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
⊢ b * a * a < a ^ (m + 1)

Tactic:
simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt

Premises used: zpow_add, zpow_one, lt_div_iff_mul_lt, div_eq_mul_inv, mul_lt_mul_iff_right, zpow_sub
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
h₁ : b * a ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
use b * a
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
h₁ : ∀ (hlt : a ^ m / a < b), a ^ m < b * a ∧ b < a ^ m
⊢ b * a ∈ Ioo (a ^ m) (a ^ (m + 1))

Tactic:
simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢

Premises used: Set.mem_Ioo, zpow_add, zpow_one, div_eq_mul_inv, mul_lt_mul_iff_right, zpow_sub
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ m / a < b
⊢ a ^ m < b * a ∧ b < a ^ m

Tactic:
⟨div_lt_iff_lt_mul.1 hlt, hm⟩

Premises used: And.intro, Iff.mp, div_lt_iff_lt_mul
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ m / a < b
⊢ a ^ m < b * a ∧ b < a ^ m

Tactic:
exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩
-- Module: Mathlib.Topology.Algebra.Order.Group
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
inst_5 : Nontrivial G
inst_6 : DenselyOrdered G
a : G
⊢ ¬DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x

Tactic:
denseRange_zpow_iff_surjective.not.mpr fun h ↦
    not_isCyclic_of_denselyOrdered G ⟨⟨a, h⟩⟩

Premises used: Iff.mpr, Iff.not, not_isCyclic_of_denselyOrdered, denseRange_zpow_iff_surjective, Exists.intro, IsCyclic.mk
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : One β
⊢ Eq (α := α → β) ((toFun : (a : α →ᵤ β) → α → β) 1 : α → β) (1 : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : One β
⊢ Eq (α := α →ᵤ β) ((ofFun : (a : α → β) → α →ᵤ β) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : One β
⊢ Eq (α := α → β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) 1 : α → β) (1 : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : One β
⊢ Eq (α := α →ᵤ[𝔖] β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Mul β
f g : α →ᵤ β
⊢ (toFun : (a : α →ᵤ β) → α → β) (f * g) =
    HMul.hMul (α := α → β) (β := α → β) ((toFun : (a : α →ᵤ β) → α → β) f : α → β)
      ((toFun : (a : α →ᵤ β) → α → β) g : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Mul β
f g : α → β
⊢ (ofFun : (a : α → β) → α →ᵤ β) (f * g) =
    HMul.hMul (α := α →ᵤ β) (β := α →ᵤ β) ((ofFun : (a : α → β) → α →ᵤ β) f : α →ᵤ β)
      ((ofFun : (a : α → β) → α →ᵤ β) g : α →ᵤ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Mul β
f g : α →ᵤ[𝔖] β
⊢ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f * g) =
    HMul.hMul (α := α → β) (β := α → β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
      ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Mul β
f g : α → β
⊢ (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) (f * g) =
    HMul.hMul (α := α →ᵤ[𝔖] β) (β := α →ᵤ[𝔖] β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f : α →ᵤ[𝔖] β)
      ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Inv β
f : α →ᵤ β
⊢ Eq (α := α → β) ((toFun : (a : α →ᵤ β) → α → β) f⁻¹ : α → β) (((toFun : (a : α →ᵤ β) → α → β) f)⁻¹ : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Inv β
f : α → β
⊢ Eq (α := α →ᵤ β) ((ofFun : (a : α → β) → α →ᵤ β) f⁻¹ : α →ᵤ β) (((ofFun : (a : α → β) → α →ᵤ β) f)⁻¹ : α →ᵤ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Inv β
f : α →ᵤ[𝔖] β
⊢ Eq (α := α → β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f⁻¹ : α → β) (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)⁻¹ : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Inv β
f : α → β
⊢ Eq (α := α →ᵤ[𝔖] β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f⁻¹ : α →ᵤ[𝔖] β)
    (((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f)⁻¹ : α →ᵤ[𝔖] β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Div β
f g : α →ᵤ β
⊢ (toFun : (a : α →ᵤ β) → α → β) (f / g) =
    HDiv.hDiv (α := α → β) (β := α → β) ((toFun : (a : α →ᵤ β) → α → β) f : α → β)
      ((toFun : (a : α →ᵤ β) → α → β) g : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Div β
f g : α → β
⊢ (ofFun : (a : α → β) → α →ᵤ β) (f / g) =
    HDiv.hDiv (α := α →ᵤ β) (β := α →ᵤ β) ((ofFun : (a : α → β) → α →ᵤ β) f : α →ᵤ β)
      ((ofFun : (a : α → β) → α →ᵤ β) g : α →ᵤ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Div β
f g : α →ᵤ[𝔖] β
⊢ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f / g) =
    HDiv.hDiv (α := α → β) (β := α → β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
      ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Div β
f g : α → β
⊢ (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) (f / g) =
    HDiv.hDiv (α := α →ᵤ[𝔖] β) (β := α →ᵤ[𝔖] β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f : α →ᵤ[𝔖] β)
      ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : SMul M β
c : M
f : α →ᵤ β
⊢ (toFun : (a : α →ᵤ β) → α → β) (c • f) = HSMul.hSMul (β := α → β) c ((toFun : (a : α →ᵤ β) → α → β) f : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : SMul M β
c : M
f : α → β
⊢ (ofFun : (a : α → β) → α →ᵤ β) (c • f) = HSMul.hSMul (β := α →ᵤ β) c ((ofFun : (a : α → β) → α →ᵤ β) f : α →ᵤ β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
M : Type u_5
inst : SMul M β
c : M
f : α →ᵤ[𝔖] β
⊢ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (c • f) =
    HSMul.hSMul (β := α → β) c ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
M : Type u_5
inst : SMul M β
c : M
f : α → β
⊢ (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) (c • f) =
    HSMul.hSMul (β := α →ᵤ[𝔖] β) c ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) f : α →ᵤ[𝔖] β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
𝔖 : Set (Set α)
x : α
M : Type u_5
N : Type u_6
inst : SMul M N
inst_1 : SMul M β
inst_2 : SMul N β
inst_3 : IsScalarTower M N β
⊢ IsScalarTower M N (α →ᵤ β)

Tactic:
inferInstanceAs <| IsScalarTower M N (α → β)

Premises used: _private.0.instIsScalarTowerUniformFun._proof_1
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
𝔖 : Set (Set α)
x : α
M : Type u_5
N : Type u_6
inst : SMul M N
inst_1 : SMul M β
inst_2 : SMul N β
inst_3 : IsScalarTower M N β
⊢ IsScalarTower M N (α →ᵤ[𝔖] β)

Tactic:
inferInstanceAs <| IsScalarTower M N (α → β)

Premises used: _private.0.instIsScalarTowerUniformOnFun._proof_1
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
𝔖 : Set (Set α)
x : α
M : Type u_5
N : Type u_6
inst : SMul M β
inst_1 : SMul N β
inst_2 : SMulCommClass M N β
⊢ SMulCommClass M N (α →ᵤ β)

Tactic:
inferInstanceAs <| SMulCommClass M N (α → β)

Premises used: _private.0.instSMulCommClassUniformFun._proof_1
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
𝔖 : Set (Set α)
x : α
M : Type u_5
N : Type u_6
inst : SMul M β
inst_1 : SMul N β
inst_2 : SMulCommClass M N β
⊢ SMulCommClass M N (α →ᵤ[𝔖] β)

Tactic:
inferInstanceAs <| SMulCommClass M N (α → β)

Premises used: _private.0.instSMulCommClassUniformOnFun._proof_1
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
𝔖 : Set (Set α)
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ IsUniformGroup (α →ᵤ G)

Tactic:
⟨(-- Since `(/) : G × G → G` is uniformly continuous,
    -- `UniformFun.postcomp_uniformContinuous` tells us that
    -- `((/) ∘ —) : (α →ᵤ G × G) → (α →ᵤ G)` is uniformly continuous too. By precomposing with
    -- `UniformFun.uniformEquivProdArrow`, this gives that
    -- `(/) : (α →ᵤ G) × (α →ᵤ G) → (α →ᵤ G)` is also uniformly continuous
    UniformFun.postcomp_uniformContinuous uniformContinuous_div).comp
    UniformFun.uniformEquivProdArrow.symm.uniformContinuous⟩

Premises used: UniformFun.uniformEquivProdArrow, UniformEquiv.symm, UniformContinuous.comp, uniformContinuous_div, UniformFun.postcomp_uniformContinuous, UniformEquiv.uniformContinuous, IsUniformGroup.mk
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (α := α →ᵤ G) (𝓝 1) p fun (i : ι) ↦ {g : α →ᵤ G | (1, g) ∈ UniformFun.gen α G {x : G × G | x.2 / x.1 ∈ b i}}

Tactic:
UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one

Premises used: Filter.HasBasis.uniformity_of_nhds_one, OfNat.ofNat, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
h₁ :
  ∀ (x : ι) (x_1 : α →ᵤ G),
    (∀ (x_2 : α), Membership.mem (α := G) (b x) ((toFun : (a : α →ᵤ G) → α → G) x_1 x_2 : G)) ↔
      (1, x_1) ∈ UniformFun.gen α G {x_2 : G × G | x_2.2 / x_2.1 ∈ b x}
⊢ HasBasis (α := α →ᵤ G) (𝓝 1) p fun (i : ι) ↦
    {f : α →ᵤ G | ∀ (x : α), Membership.mem (α := G) (b i) ((toFun : (a : α →ᵤ G) → α → G) f x : G)}

Tactic:
convert! UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one

Premises used: Filter.HasBasis.uniformity_of_nhds_one, OfNat.ofNat, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
x : ι
x_1 : α →ᵤ G
⊢ (∀ (x_2 : α), Membership.mem (α := G) (b x) ((toFun : (a : α →ᵤ G) → α → G) x_1 x_2 : G)) ↔
    (1, x_1) ∈ UniformFun.gen α G {x_2 : G × G | x_2.2 / x_2.1 ∈ b x}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ HasBasis (α := α →ᵤ G) (𝓝 1) (fun (V : Set G) ↦ Membership.mem (γ := Filter G) (𝓝 1) V) fun (V : Set G) ↦
    {f : α → G | ∀ (x : α), f x ∈ V}

Tactic:
UniformFun.hasBasis_nhds_one_of_basis (basis_sets _)

Premises used: Set.Mem, setOf, UniformFun.hasBasis_nhds_one_of_basis, Filter.basis_sets, UniformFun
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
𝔖 : Set (Set α)
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ IsUniformGroup (α →ᵤ[𝔖] G)

Tactic:
⟨(-- Since `(/) : G × G → G` is uniformly continuous,
    -- `UniformOnFun.postcomp_uniformContinuous` tells us that
    -- `((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G)` is uniformly continuous too. By precomposing with
    -- `UniformOnFun.uniformEquivProdArrow`, this gives that
    -- `(/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G)` is also uniformly continuous
    UniformOnFun.postcomp_uniformContinuous uniformContinuous_div).comp
    UniformOnFun.uniformEquivProdArrow.symm.uniformContinuous⟩

Premises used: UniformOnFun.uniformEquivProdArrow, UniformOnFun.postcomp_uniformContinuous, UniformEquiv.symm, UniformContinuous.comp, uniformContinuous_div, UniformEquiv.uniformContinuous, IsUniformGroup.mk
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (α := α →ᵤ[𝔖] G) (𝓝 1) (fun (Si : Prod.{u_1, u_3} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2)
    fun (Si : Prod.{u_1, u_3} (Set α) ι) ↦
    {g : α →ᵤ[𝔖] G |
      Membership.mem (γ := Set ((α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G))) (UniformOnFun.gen 𝔖 Si.1 {x : G × G | x.1 / x.2 ∈ b Si.2})
        (g, 1)}

Tactic:
UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
      h.uniformity_of_nhds_one_swapped

Premises used: UniformOnFun.hasBasis_nhds_of_basis, Filter.HasBasis.uniformity_of_nhds_one_swapped, OfNat.ofNat