awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)

Tactic:
have : Tendsto (fun u => -(c • u : V) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p) :=
    Continuous.tendsto' (by fun_prop) _ _ (by simp)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
h :
  ∀ (ht : 0 < t),
    Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
      (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
⊢ 0 < (t, u).1 →
    Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
      (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s

Tactic:
(ht : 0 < t)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
h : ∀ (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s), (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
⊢ Membership.mem (γ := Set (k × V)) ((fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) ∘ Prod.snd ⁻¹' s) (t, u) →
    (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s

Tactic:
(hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : ∀ (h : t • u +ᵥ c • v +ᵥ p ∈ s), c • v +ᵥ p ∈ s
⊢ (t, u).1 • (t, u).2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s

Tactic:
(h : t • u +ᵥ c • v +ᵥ p ∈ s)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
h : ∀ (t : k) (u : V) (ht : 0 < t) (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s), c • v +ᵥ p ∈ s
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s

Tactic:
filter_upwards [tendsto_fst.eventually <| eventually_gt_atTop 0, this.comp tendsto_snd hp]
    with ⟨t, u⟩ (ht : 0 < t) (hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s) (h : t • u +ᵥ c • v +ᵥ p ∈ s)

Premises used: Filter.Tendsto.eventually, Filter.Tendsto.comp, OfNat.ofNat, Filter.tendsto_snd, Filter.tendsto_fst, Filter.eventually_gt_atTop
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
h₁ : c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]
⊢ c • v +ᵥ p ∈ s

Tactic:
apply hs.segment_subset hu h

Premises used: Convex.segment_subset
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
h₁ : SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))
⊢ c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]

Tactic:
simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub]

Premises used: mem_segment_iff_sameRay, vsub_eq_sub
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
h₁ : SameRay k (c • u) (t • u)
⊢ SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))

Tactic:
rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_neg, vadd_vsub]

Premises used: vsub_vadd_eq_vsub_sub, neg_neg, vadd_vsub, vsub_self, zero_sub
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k (c • u) (t • u)

Tactic:
(SameRay.sameRay_nonneg_smul_left _ hc).pos_smul_right ht

Premises used: SameRay.sameRay_nonneg_smul_left, SameRay.pos_smul_right
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k (c • u) (t • u)

Tactic:
exact (SameRay.sameRay_nonneg_smul_left _ hc).pos_smul_right ht

Premises used: SameRay.sameRay_nonneg_smul_left, SameRay.pos_smul_right
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
⊢ (↑((of G).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) = G

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A : ProfiniteGrp.{u}
⊢ Hom.hom (𝟙 A) =
    ContinuousMonoidHom.id
      (↑(A.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)

Tactic:
rfl

Premises used: ContinuousMonoidHom.id, rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A : ProfiniteGrp.{u}
a : (↑(A.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (Hom.hom (𝟙 A) : (a : (↑A.toProfinite.toTop : Type u)) → (↑A.toProfinite.toTop : Type u)) a = a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: ContinuousMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
a : (↑(A.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Eq (α := (↑(C.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom (f ≫ g) : (a : (↑A.toProfinite.toTop : Type u)) → (↑C.toProfinite.toTop : Type u)) a :
      (↑(C.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom g : (a : (↑B.toProfinite.toTop : Type u)) → (↑C.toProfinite.toTop : Type u))
        ((Hom.hom f : (a : (↑A.toProfinite.toTop : Type u)) → (↑B.toProfinite.toTop : Type u)) a :
          (↑(B.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) :
      (↑(C.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
simp only [hom_comp, ContinuousMonoidHom.comp_toFun]

Premises used: ProfiniteGrp.hom_comp, ContinuousMonoidHom.comp_toFun
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B : ProfiniteGrp.{u}
f g : A ⟶ B
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: ProfiniteGrp.Hom.ext
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
f : X →ₜ* Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B : ProfiniteGrp.{u}
f : A ⟶ B
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
⊢ ofHom (ContinuousMonoidHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
f : X →ₜ* Y
g : Y →ₜ* Z
⊢ Eq (α := of X ⟶ of Z) (ofHom (g.comp f)) (CategoryStruct.comp (Y := of Y) (ofHom f) (ofHom g))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
f : X →ₜ* Y
x : X
⊢ Eq (α :=
    (↑((of Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((Hom.hom (ofHom f) : (a : (↑(of X).toProfinite.toTop : Type u)) → (↑(of Y).toProfinite.toTop : Type u)) x :
      (↑((of Y).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B : ProfiniteGrp.{u}
e : A ≅ B
x : (↑(A.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (Hom.hom e.inv : (a : (↑B.toProfinite.toTop : Type u)) → (↑A.toProfinite.toTop : Type u))
      ((Hom.hom e.hom : (a : (↑A.toProfinite.toTop : Type u)) → (↑B.toProfinite.toTop : Type u)) x :
        (↑(B.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
A B : ProfiniteGrp.{u}
e : A ≅ B
x : (↑(B.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ (Hom.hom e.hom : (a : (↑A.toProfinite.toTop : Type u)) → (↑B.toProfinite.toTop : Type u))
      ((Hom.hom e.inv : (a : (↑B.toProfinite.toTop : Type u)) → (↑A.toProfinite.toTop : Type u)) x :
        (↑(A.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X : ProfiniteGrp.{u_1}
⊢ Eq (α :=
    (a :
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1)) →
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
    (⇑(Hom.hom (𝟙 X)) : (a : (↑X.toProfinite.toTop : Type u_1)) → (↑X.toProfinite.toTop : Type u_1)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : ProfiniteGrp.{u_1}
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (a :
        (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1)) →
      (↑(Z.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
    (⇑(Hom.hom (f ≫ g)) : (a : (↑X.toProfinite.toTop : Type u_1)) → (↑Z.toProfinite.toTop : Type u_1))
    (Function.comp (β :=
      (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
      (⇑(Hom.hom g) : (a : (↑Y.toProfinite.toTop : Type u_1)) → (↑Z.toProfinite.toTop : Type u_1))
      (⇑(Hom.hom f) : (a : (↑X.toProfinite.toTop : Type u_1)) → (↑Y.toProfinite.toTop : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
G H : FiniteGrp.{u}
f : G ⟶ H
⊢ Continuous
    (↑(GrpCat.Hom.hom f.hom) :
        OneHom (↑(ofFiniteGrp G).toProfinite.toTop : Type u) (↑(ofFiniteGrp H).toProfinite.toTop : Type u)).toFun

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
X_1 Y_1 : ProfiniteGrp.{u_1}
f : X_1 ⟶ Y_1
⊢ Continuous (X := (↑X_1.1.1 : Type u_1)) (Y := (↑Y_1.1.1 : Type u_1))
    (⇑(Hom.hom f) : (a : (↑X_1.toProfinite.toTop : Type u_1)) → (↑Y_1.toProfinite.toTop : Type u_1))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
⊢ Functor.Faithful
    (forget₂ ProfiniteGrp.{u_1} (FC := fun (X Y : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1) →ₜ*
        (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1))
      (CC := fun (X : ProfiniteGrp.{u_1}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
        Type u_1))
      Profinite (FD :=
      fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
        (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
      (CD := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))

Tactic:
{
  map_injective := fun {_ _} _ _ h =>
    ConcreteCategory.hom_ext _ _ fun x ↦ CategoryTheory.congr_fun h x }

Premises used: CategoryTheory.Functor.Faithful.mk, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : TopologicalSpace X
inst_2 : IsTopologicalGroup X
inst_3 : CompactSpace X
inst_4 : TotallyDisconnectedSpace X
inst_5 : Group Y
inst_6 : TopologicalSpace Y
inst_7 : IsTopologicalGroup Y
inst_8 : CompactSpace Y
inst_9 : TotallyDisconnectedSpace Y
inst_10 : Group Z
inst_11 : TopologicalSpace Z
inst_12 : IsTopologicalGroup Z
inst_13 : CompactSpace Z
inst_14 : TotallyDisconnectedSpace Z
⊢ Functor.ReflectsIsomorphisms
    (forget ProfiniteGrp.{u} (FC := fun (X Y : ProfiniteGrp.{u}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
        (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (CC := fun (X : ProfiniteGrp.{u}) ↦
      (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))

Tactic:
CategoryTheory.reflectsIsomorphisms_comp (forget₂ ProfiniteGrp Profinite) (forget Profinite)

Premises used: CategoryTheory.reflectsIsomorphisms_comp, CategoryTheory.Functor.comp, ProfiniteGrp, CategoryTheory.forget₂, Profinite, CategoryTheory.forget
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
a b :
  (j : J) →
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v))
hx :
  Membership.mem (γ :=
    Set
      ((j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))))
    {x :
      (j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v)) |
      ∀ ⦃i j : J⦄ (π : i ⟶ j),
        (Hom.hom (F.map π) :
              (a : (↑(F.obj i).toProfinite.toTop : Type (max u v))) → (↑(F.obj j).toProfinite.toTop : Type (max u v)))
            (x i) =
          x j}
    a
hy :
  Membership.mem (γ :=
    Set
      ((j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))))
    {x :
      (j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v)) |
      ∀ ⦃i j : J⦄ (π : i ⟶ j),
        (Hom.hom (F.map π) :
              (a : (↑(F.obj i).toProfinite.toTop : Type (max u v))) → (↑(F.obj j).toProfinite.toTop : Type (max u v)))
            (x i) =
          x j}
    b
x x_1 : J
π : x ⟶ x_1
⊢ (Hom.hom (F.map π) :
        (a : (↑(F.obj x).toProfinite.toTop : Type (max u v))) → (↑(F.obj x_1).toProfinite.toTop : Type (max u v)))
      ((a * b) x) =
    (a * b) x_1

Tactic:
simp only [Pi.mul_apply, map_mul, hx π, hy π]

Premises used: Pi.mul_apply, map_mul
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
⊢ Membership.mem (γ :=
    Set
      ((j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))))
    {x :
      (j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v)) |
      ∀ ⦃i j : J⦄ (π : i ⟶ j),
        (Hom.hom (F.map π) :
              (a : (↑(F.obj i).toProfinite.toTop : Type (max u v))) → (↑(F.obj j).toProfinite.toTop : Type (max u v)))
            (x i) =
          x j}
    1

Tactic:
simp only [Set.mem_setOf_eq, Pi.one_apply, map_one, implies_true]

Premises used: Pi.one_apply, Set.mem_setOf_eq, map_one, implies_true
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
x :
  (j : J) →
    (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
      Type (max u v))
h :
  Membership.mem (γ :=
    Set
      ((j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v))))
    {x :
      (j : J) →
        (↑((F.obj j).toProfinite.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
          Type (max u v)) |
      ∀ ⦃i j : J⦄ (π : i ⟶ j),
        (Hom.hom (F.map π) :
              (a : (↑(F.obj i).toProfinite.toTop : Type (max u v))) → (↑(F.obj j).toProfinite.toTop : Type (max u v)))
            (x i) =
          x j}
    x
x_1 x_2 : J
π : x_1 ⟶ x_2
⊢ (Hom.hom (F.map π) :
        (a : (↑(F.obj x_1).toProfinite.toTop : Type (max u v))) → (↑(F.obj x_2).toProfinite.toTop : Type (max u v)))
      (x⁻¹ x_1) =
    x⁻¹ x_2

Tactic:
simp only [Pi.inv_apply, map_inv, h π]

Premises used: map_inv, Pi.inv_apply