awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
x : ι
⊢ Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)

Tactic:
map_one _

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
x : ι
⊢ Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)

Tactic:
exact map_one _

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
h :
  ∀ (x : ι),
    swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
      HMul.hMul (α := ι → M) (β := ι → M)
        (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
        (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) =
    HMul.hMul (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
x : ι
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x

Tactic:
map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
x : ι
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x

Tactic:
exact map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
φ : G →* ι →ᵤ M :=
  { toFun := swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F), map_one' := ⋯,
    map_mul' := ⋯ }
⊢ Continuous (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))

Tactic:
continuous_of_continuousAt_one φ hf

Premises used: continuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
φ : G →* ι →ᵤ M :=
  { toFun := swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F), map_one' := ⋯,
    map_mul' := ⋯ }
⊢ Continuous (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))

Tactic:
exact continuous_of_continuousAt_one φ hf

Premises used: continuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
rw :
  UniformContinuous (α := G) (β := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
⊢ UniformEquicontinuous.{u_1, u_3, u_2} (α := M) (β := G) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]

Premises used: uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1

Tactic:
rw [equicontinuousAt_iff_continuousAt] at hf

Premises used: equicontinuousAt_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
h :
  ∀ (x : ι),
    Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)
⊢ Eq (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1) 1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
x : ι
⊢ Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)

Tactic:
map_one _

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
x : ι
⊢ Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)

Tactic:
exact map_one _

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
h :
  ∀ (x : ι),
    swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
      HMul.hMul (α := ι → M) (β := ι → M)
        (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
        (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) =
    HMul.hMul (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
x : ι
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x

Tactic:
map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
x : ι
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x

Tactic:
exact map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
φ : G →* ι →ᵤ M :=
  { toFun := swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F), map_one' := ⋯,
    map_mul' := ⋯ }
⊢ UniformContinuous (α := G) (β := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))

Tactic:
uniformContinuous_of_continuousAt_one φ hf

Premises used: uniformContinuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.Equicontinuity
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
φ : G →* ι →ᵤ M :=
  { toFun := swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F), map_one' := ⋯,
    map_mul' := ⋯ }
⊢ UniformContinuous (α := G) (β := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))

Tactic:
exact uniformContinuous_of_continuousAt_one φ hf

Premises used: uniformContinuous_of_continuousAt_one
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
a : K
ha : a ≠ 0
⊢ Tendsto (fun (x : K) ↦ a * x) (cocompact K) (cocompact K)

Tactic:
Filter.tendsto_cocompact_mul_left (inv_mul_cancel₀ ha)

Premises used: Filter.tendsto_cocompact_mul_left, inv_mul_cancel₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
a : K
ha : a ≠ 0
⊢ Tendsto (fun (x : K) ↦ x * a) (cocompact K) (cocompact K)

Tactic:
Filter.tendsto_cocompact_mul_right (mul_inv_cancel₀ ha)

Premises used: mul_inv_cancel₀, Filter.tendsto_cocompact_mul_right
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
this : DiscreteTopology K
⊢ Finite K

Tactic:
finite_of_compact_of_discrete

Premises used: finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
this : DiscreteTopology K
⊢ Finite K

Tactic:
exact finite_of_compact_of_discrete

Premises used: finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
suffices : DiscreteTopology K
⊢ Finite K

Tactic:
suffices DiscreteTopology K by
    exact finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
rw : IsOpen (X := K) {0}
⊢ DiscreteTopology K

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero]

Premises used: discreteTopology_iff_isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
⊢ IsOpen (X := K) {0}

Tactic:
GroupWithZero.isOpen_singleton_zero

Premises used: GroupWithZero.isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
⊢ IsOpen (X := K) {0}

Tactic:
exact GroupWithZero.isOpen_singleton_zero

Premises used: GroupWithZero.isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
inl : ∀ (hx : 0 ∈ closure (↑K : Set α)), 0⁻¹ ∈ closure (↑K : Set α)
inr : ∀ (h : x ≠ 0), x⁻¹ ∈ closure (↑K : Set α)
⊢ x⁻¹ ∈ closure (↑K : Set α)

Tactic:
rcases eq_or_ne x 0 with (rfl | h)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
hx : 0 ∈ closure (↑K : Set α)
inl inl₁ inl₂ inl₃ : 0 ∈ closure (↑K : Set α)
⊢ 0⁻¹ ∈ closure (↑K : Set α)

Tactic:
rwa [inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
h : x ≠ 0
inr : Membership.mem (γ := Set α) (closure ((fun (x : α) ↦ x⁻¹) '' (↑K : Set α))) x⁻¹
⊢ x⁻¹ ∈ closure (↑K : Set α)

Tactic:
rw [← inv_coe_set, ← Set.image_inv_eq_inv]

Premises used: inv_coe_set, Set.image_inv_eq_inv
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
h : x ≠ 0
⊢ Membership.mem (γ := Set α) (closure ((fun (x : α) ↦ x⁻¹) '' (↑K : Set α))) x⁻¹

Tactic:
mem_closure_image (continuousAt_inv₀ h) hx

Premises used: ContinuousInv₀.continuousAt_inv₀, Set.Mem, mem_closure_image
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
h : x ≠ 0
⊢ Membership.mem (γ := Set α) (closure ((fun (x : α) ↦ x⁻¹) '' (↑K : Set α))) x⁻¹

Tactic:
exact mem_closure_image (continuousAt_inv₀ h) hx

Premises used: ContinuousInv₀.continuousAt_inv₀, mem_closure_image
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
inst : Field α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalDivisionRing α
s : Subfield α
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
inst : Field α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalDivisionRing α
s : Subfield α
⊢ IsClosed (↑s.topologicalClosure : Set α)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
inst : Field α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalDivisionRing α
s t : Subfield α
h : s ≤ t
ht : IsClosed (↑t : Set α)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
rw :
  Continuous (X := { r : R // 0 ≤ r }ˣ)
    (Subtype.val (p := fun (r : R) ↦ 0 < r) ∘ Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) :
      { r : R // 0 ≤ r }ˣ → R)
⊢ Continuous (X := { r : R // 0 ≤ r }ˣ)
    (Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 ≤ r }ˣ → { r : R // 0 < r })

Tactic:
rw [Topology.IsEmbedding.subtypeVal.continuous_iff]

Premises used: Topology.IsEmbedding.subtypeVal, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
⊢ Continuous (X := { r : R // 0 ≤ r }ˣ)
    (Subtype.val (p := fun (r : R) ↦ 0 < r) ∘ Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) :
      { r : R // 0 ≤ r }ˣ → R)

Tactic:
Continuous.subtype_val (p := (0 ≤ ·)) Units.continuous_val

Premises used: Units.continuous_val, Continuous.subtype_val
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
⊢ Continuous (X := { r : R // 0 ≤ r }ˣ)
    (Subtype.val (p := fun (r : R) ↦ 0 < r) ∘ Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) :
      { r : R // 0 ≤ r }ˣ → R)

Tactic:
exact Continuous.subtype_val (p := (0 ≤ ·)) Units.continuous_val
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
rw :
  Continuous (X := { r : R // 0 < r })
      (Function.comp (β := { r : R // 0 ≤ r }ˣ) (Units.val : (self : { r : R // 0 ≤ r }ˣ) → { r : R // 0 ≤ r })
        (Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 < r } → { r : R // 0 ≤ r }ˣ)) ∧
    Continuous (Y := { r : R // 0 ≤ r }) fun (x : { r : R // 0 < r }) ↦
      (↑((Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) x)⁻¹ : { r : R // 0 ≤ r }ˣ) : { r : R // 0 ≤ r })
⊢ Continuous (X := { r : R // 0 < r }) (Y := { r : R // 0 ≤ r }ˣ)
    (Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 < r } → { r : R // 0 ≤ r }ˣ)

Tactic:
rw [Units.continuous_iff]

Premises used: Units.continuous_iff
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
⊢ Continuous (X := { r : R // 0 < r })
    (Function.comp (β := { r : R // 0 ≤ r }ˣ) (Units.val : (self : { r : R // 0 ≤ r }ˣ) → { r : R // 0 ≤ r })
      (Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 < r } → { r : R // 0 ≤ r }ˣ))

Tactic:
fun_prop