awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)

Tactic:
Filter.Tendsto.cauchy_map <|
      calc
        map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
        _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx'

Premises used: Filter.map_mono, Trans.trans, ContinuousInv₀.continuousAt_inv₀, Filter.Tendsto.cauchy_map
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)

Tactic:
exact Filter.Tendsto.cauchy_map <|
      calc
        map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
        _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx'

Premises used: Filter.map_mono, ContinuousInv₀.continuousAt_inv₀, Filter.map, nhds, Inv.inv, Filter.Tendsto.cauchy_map
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ CompletableTopField α

Tactic:
CompletableTopField.mk (fun F F_cau inf_F => ?_)

Premises used: CompletableTopField.mk
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
refine : ∀ (F : Filter α) (F_cau : Cauchy F) (inf_F : 𝓝 0 ⊓ F = ⊥), Cauchy (α := α) (map (fun (x : α) ↦ x⁻¹) F)
⊢ CompletableTopField α

Tactic:
refine CompletableTopField.mk (fun F F_cau inf_F => ?_)

Premises used: CompletableTopField.mk
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
rw :
  ∀ (F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)) (inf_F : 𝓝 0 ⊓ F = ⊥),
    Cauchy.{u_4} (α := β) (map (α := α) (⇑f : (a : α) → β) (map (fun (x : α) ↦ x⁻¹) F))
⊢ Cauchy (α := α) (map (fun (x : α) ↦ x⁻¹) F)

Tactic:
rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢

Premises used: IsUniformInducing.cauchy_map_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := β) (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ x⁻¹) x)
      (((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β)) x)
⊢ Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x : α
⊢ Eq.{u_4 + 1} (α := β) (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ x⁻¹) x)
    (((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β)) x)

Tactic:
simp only [Function.comp_apply, map_inv₀]

Premises used: map_inv₀, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))

Tactic:
have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
    ext; simp only [Function.comp_apply, map_inv₀]
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw : Cauchy.{u_4} (α := β) (map (fun (x : β) ↦ x⁻¹) (map (⇑f : (a : α) → β) F))
⊢ Cauchy.{u_4} (α := β) (map (α := α) (⇑f : (a : α) → β) (map (fun (x : α) ↦ x⁻¹) F))

Tactic:
rw [Filter.map_comm h_comm]

Premises used: Filter.map_comm
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
apply : Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
⊢ Cauchy.{u_4} (α := β) (map (fun (x : β) ↦ x⁻¹) (map (⇑f : (a : α) → β) F))

Tactic:
apply CompletableTopField.nice _ F_cau

Premises used: CompletableTopField.nice
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw :
  Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F))
    ⊥
rw₁ :
  Eq.{u_4 + 1} (α := Filter β)
    (map (⇑f : (a : α) → β)
      (Filter.comap.{u_3, u_4} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 ((f : (a : α) → β) 0) : Filter β) ⊓ F))
    ⊥
rw₂ : Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (𝓝 0 ⊓ F)) ⊥
rw₃ : Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑f : (a : α) → β) ⊥) ⊥
rw₄ rw₅ : Eq.{u_4 + 1} (α := Filter β) ⊥ ⊥
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥

Tactic:
rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.map_bot, Filter.push_pull', map_zero, IsUniformInducing.isInducing
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
⊢ IsUniformAddGroup G

Tactic:
@isUniformAddGroup_of_addCommGroup G _ B.topology B.isTopologicalAddGroup

Premises used: isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this : UniformSpace G := B.uniformSpace
⊢ IsUniformAddGroup G

Tactic:
haveI := B.isUniformAddGroup
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
⟨h', ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
mp : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
refine ⟨h', ?_⟩
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F

Tactic:
⟨h', ?_⟩

Premises used: Cauchy, And.intro
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : F ×ˢ F ≤ uniformity G
⊢ Cauchy F

Tactic:
refine ⟨h', ?_⟩
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
mp mp₁ mp₂ mp₃ : F ×ˢ F ≤ uniformity G
⊢ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
rwa [← this]
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h mpr mpr₁ mpr₂ mpr₃ : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ F ×ˢ F ≤ uniformity G

Tactic:
rwa [this]
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₁ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₁ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₂ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₂ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₃ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₃ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₄ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₄ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₅ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₅ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₆ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₆ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₇ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₇ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₈ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₈ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), F ×ˢ F ≤ uniformity G
mp₉ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₉ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), F ×ˢ F ≤ uniformity G
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
suffices : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U by
    constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
rw :
  LE.le (α := Filter G) (map (fun (x : G × G) ↦ x.2 - x.1) (F ×ˢ F)) (nhds 0) ↔
    ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]

Premises used: uniformity_eq_comap_nhds_zero, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.Algebra.UniformFilterBasis
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
⊢ Tendsto (β := G) (fun (x : G × G) ↦ x.2 - x.1) (F ×ˢ F) (nhds 0) ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_comm (_ ∈ _) G]

Premises used: Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, forall_comm, AddGroupFilterBasis.nhds_zero_hasBasis, Filter.basis_sets
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : AddGroup X
inst_3 : IsUniformAddGroup X
⊢ UniformContinuousConstSMul ℕ X

Tactic:
⟨uniformContinuous_const_nsmul⟩

Premises used: UniformContinuousConstSMul.mk, uniformContinuous_const_nsmul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : AddGroup X
inst_3 : IsUniformAddGroup X
⊢ UniformContinuousConstSMul ℤ X

Tactic:
⟨uniformContinuous_const_zsmul⟩

Premises used: UniformContinuousConstSMul.mk, uniformContinuous_const_zsmul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
inst : AddGroup M
inst_1 : DistribSMul R M
inst_2 : UniformSpace M
inst_3 : IsUniformAddGroup M
inst_4 : ContinuousConstSMul R M
⊢ UniformContinuousConstSMul R M

Tactic:
⟨fun r =>
    uniformContinuous_of_continuousAt_zero (DistribSMul.toAddMonoidHom M r)
      (Continuous.continuousAt (continuous_const_smul r))⟩

Premises used: ContinuousConstSMul.continuous_const_smul, UniformContinuousConstSMul.mk, uniformContinuous_of_continuousAt_zero, Continuous.continuousAt, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : Ring R
inst_3 : UniformSpace R
inst_4 : IsUniformAddGroup R
inst_5 : ContinuousMul R
⊢ UniformContinuousConstSMul R R

Tactic:
uniformContinuousConstSMul_of_continuousConstSMul _ _

Premises used: uniformContinuousConstSMul_of_continuousConstSMul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : Ring R
inst_3 : UniformSpace R
inst_4 : IsUniformAddGroup R
inst_5 : ContinuousMul R
⊢ UniformContinuousConstSMul Rᵐᵒᵖ R

Tactic:
uniformContinuousConstSMul_of_continuousConstSMul _ _

Premises used: uniformContinuousConstSMul_of_continuousConstSMul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : UniformContinuousConstSMul M X
⊢ ContinuousConstSMul M X

Tactic:
⟨fun c => (uniformContinuous_const_smul c).continuous⟩

Premises used: ContinuousConstSMul.mk, UniformContinuous.continuous, UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : UniformContinuousConstSMul M X
f : Y → X
hf : UniformContinuous f
c : M
⊢ UniformContinuous (c • f)

Tactic:
(uniformContinuous_const_smul c).comp hf

Premises used: UniformContinuous.comp, UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul M Y
inst_4 : UniformContinuousConstSMul M Y
f : X → Y
hf : IsUniformInducing f
hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x
c : M
⊢ UniformContinuous (β := X) fun (x : X) ↦ c • x

Tactic:
simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
      using hf.uniformContinuous.const_smul c

Premises used: Function.comp_def, IsUniformInducing.uniformContinuous_iff, UniformContinuous.const_smul, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul.{v, x} Mᵐᵒᵖ X
inst_4 : IsCentralScalar M X
inst_5 : UniformContinuousConstSMul M X
c : M
⊢ UniformContinuous (β := X) fun (x : X) ↦ MulOpposite.op c • x

Tactic:
simpa only [op_smul_eq_smul] using uniformContinuous_const_smul c

Premises used: IsCentralScalar.op_smul_eq_smul, UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : UniformContinuousConstSMul M X
⊢ UniformContinuousConstSMul.{v, x} M Xᵐᵒᵖ

Tactic:
⟨fun c =>
    MulOpposite.uniformContinuous_op.comp <| MulOpposite.uniformContinuous_unop.const_smul c⟩

Premises used: UniformContinuousConstSMul.mk, UniformContinuous.comp, MulOpposite.uniformContinuous_op, UniformContinuous.const_smul, MulOpposite.uniformContinuous_unop
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
G : Type u
inst_2 : Group G
inst_3 : UniformSpace G
inst_4 : IsUniformGroup G
⊢ UniformContinuousConstSMul G G

Tactic:
⟨fun _ => uniformContinuous_const.mul uniformContinuous_id⟩

Premises used: UniformContinuousConstSMul.mk, uniformContinuous_id, uniformContinuous_const, UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_1
β : Type u_2
inst : Ring R
inst_1 : UniformSpace R
inst_2 : UniformSpace β
inst_3 : UniformContinuousConstSMul R R
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous.{u_2, u_1} (β := R) fun (x : β) ↦ a * f x

Tactic:
hf.const_smul a

Premises used: UniformContinuous.const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_1
β : Type u_2
inst : Ring R
inst_1 : UniformSpace R
inst_2 : UniformSpace β
inst_3 : UniformContinuousConstSMul Rᵐᵒᵖ R
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous.{u_2, u_1} (β := R) fun (x : β) ↦ f x * a

Tactic:
hf.const_smul (MulOpposite.op a)

Premises used: MulOpposite.unop, UniformContinuous.const_smul, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_1
inst : Ring R
inst_1 : UniformSpace R
inst_2 : UniformContinuousConstSMul R R
a : R
⊢ UniformContinuous (β := R) fun (b : R) ↦ a * b

Tactic:
uniformContinuous_id.const_mul' _

Premises used: UniformContinuous.const_mul', uniformContinuous_id
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_1
inst : Ring R
inst_1 : UniformSpace R
inst_2 : UniformContinuousConstSMul Rᵐᵒᵖ R
a : R
⊢ UniformContinuous (β := R) fun (b : R) ↦ b * a

Tactic:
uniformContinuous_id.mul_const' _

Premises used: uniformContinuous_id, UniformContinuous.mul_const'
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_3
β : Type u_4
inst : DivisionRing R
inst_1 : UniformSpace R
inst_2 : UniformContinuousConstSMul Rᵐᵒᵖ R
inst_3 : UniformSpace β
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous.{u_4, u_3} (β := R) fun (x : β) ↦ f x / a

Tactic:
simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹

Premises used: div_eq_mul_inv, Inv.inv, UniformContinuous.mul_const'
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u_3
inst : DivisionRing R
inst_1 : UniformSpace R
inst_2 : UniformContinuousConstSMul Rᵐᵒᵖ R
a : R
⊢ UniformContinuous (β := R) fun (b : R) ↦ b / a

Tactic:
uniformContinuous_id.div_const' _

Premises used: uniformContinuous_id, UniformContinuous.div_const'
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
inst : UniformSpace X
inst_1 : Monoid M
inst_2 : MulAction M X
inst_3 : UniformContinuousConstSMul M X
c : M
hc : IsUnit c
d : M
hcd : c * d = 1
cU : c • 𝓤 X ≤ 𝓤 X
dU : d • 𝓤 X ≤ 𝓤 X
⊢ 𝓤 X ≤ c • 𝓤 X

Tactic:
simpa [smul_smul, hcd] using Filter.smul_filter_le_smul_filter (a := c) dU

Premises used: smul_smul, Filter.smul_filter_le_smul_filter
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
inst : UniformSpace X
inst_1 : Group M
inst_2 : MulAction M X
inst_3 : UniformContinuousConstSMul M X
c : M
⊢ c • 𝓤 X = 𝓤 X

Tactic:
Group.isUnit _ |>.smul_uniformity

Premises used: Group.isUnit, IsUnit.smul_uniformity
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
inst : UniformSpace X
inst_1 : GroupWithZero M
inst_2 : MulAction M X
inst_3 : UniformContinuousConstSMul M X
c : M
hc : c ≠ 0
⊢ c • 𝓤 X = 𝓤 X

Tactic:
hc.isUnit.smul_uniformity

Premises used: Ne.isUnit, IsUnit.smul_uniformity
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
inst : UniformSpace X
inst_1 : SMul M X
c : M
x : Completion X
⊢ c • x = Completion.map (fun (x : X) ↦ c • x) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
⊢ UniformContinuousConstSMul.{v, x} M (Completion X)

Tactic:
⟨fun _ => uniformContinuous_map⟩

Premises used: UniformContinuousConstSMul.mk, UniformSpace.Completion.uniformContinuous_map