awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
s : S
y : Y
⊢ y ∈ preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s} ↔ y ∈ C s

Tactic:
simp [preimage_liftCover]

Premises used: Set.preimage_liftCover
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
refine_2 : ∀ (y : Y), (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y
⊢ f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ = g'

Tactic:
ext y
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
y : Y
⊢ Membership.mem (γ := Set Y) (⋃ (i : S), C i) y

Tactic:
simp [C_cover_univ]
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
y : Y
⊢ Membership.mem (γ := Set Y) (⋃ (i : S), C i) y

Tactic:
have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ]
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
y : Y
hy : Membership.mem (γ := Set Y) (⋃ (i : S), C i) y
refine_2 :
  ∀ (i : S) (hi : y ∈ C i), (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y
⊢ (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y

Tactic:
obtain ⟨i, hi⟩ := mem_iUnion.mp hy

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
y : Y
hy : Membership.mem (γ := Set Y) (⋃ (i : S), C i) y
i : S
hi : y ∈ C i
⊢ (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y

Tactic:
simpa [liftCover_of_mem hi] using symm (C_subset_D i hi)

Premises used: Set.liftCover_of_mem, symm
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
refine_3 : ∀ (x : X), (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f) x = g x
⊢ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f = g

Tactic:
ext x
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
x : X
⊢ f x ∈ Z (g x)

Tactic:
simpa [mem_image] using ⟨x, rfl, rfl⟩

Premises used: Set.mem_image
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : TopologicalSpace Y
inst_3 : CompactSpace Y
inst_4 : T2Space Y
inst_5 : TotallyDisconnectedSpace Y
inst_6 : TopologicalSpace S
inst_7 : T2Space S
inst_8 : Finite S
inst_9 : TopologicalSpace T
inst_10 : T2Space T
f : X → Y
hf : Continuous[inst, inst_2] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst, inst_6] g
g' : Y → T
hg' : Continuous[inst_2, inst_9] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun (i : S) ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst_2] (Z i)
Z_disj : PairwiseDisjoint univ Z
D : S → Set Y := fun (i : S) ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : Subset.{u_2} (α := Set Y) (⋃ (i : S), D i) (⋃ (i : S), C i)
C_disj : PairwiseDisjoint univ C
D_cover_univ : Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)
C_cover_univ : Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ
h_glue : ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j
x : X
⊢ (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f) x = g x

Tactic:
simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)]

Premises used: Set.liftCover_of_mem
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X Y S T : Profinite
inst : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f : X ⟶ Y
inst_1 : Mono f
f' : S ⟶ T
inst_2 : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous (X :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X Y S T : Profinite
inst : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f : X ⟶ Y
inst_1 : Mono f
f' : S ⟶ T
inst_2 : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous (X :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      S)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) S)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
X Y S T : Profinite
inst : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f : X ⟶ Y
inst_1 : Mono f
f' : S ⟶ T
inst_2 : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
⊢ Continuous (X :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      T)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g') :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) T)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : Profinite
inst : Nonempty.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_1 : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
⊢ ∀ (T : Profinite.{u})
    [Nonempty.{u + 1} (↑(T.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)],
    IsSplitEpi (Y := CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
      (IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) T)

Tactic:
have (T : Profinite.{u}) [Nonempty T] : IsSplitEpi (CompHausLike.isTerminalPUnit.from T) :=
      IsSplitEpi.mk' { section_ := CompHausLike.const _ (Nonempty.some inferInstance) }
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : Profinite
inst : Nonempty.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_1 : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
this :
  ∀ (T : Profinite.{u})
    [Nonempty.{u + 1} (↑(T.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)],
    IsSplitEpi (Y := CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
      (IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) T)
obtain :
  ∀ (k : Y ⟶ S),
    Eq (α := Y ⟶ CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
        (k ≫
          IsTerminal.from
            (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) S)
        (IsTerminal.from
          (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) Y) →
      ∀ (h2 : f ≫ k = g), ∃ (h : Y ⟶ S), f ≫ h = g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
obtain ⟨k, _, h2⟩ := exists_lift_of_finite_of_mono_of_epi f
        (CompHausLike.isTerminalPUnit.from S) g (CompHausLike.isTerminalPUnit.from Y)
      (CompHausLike.isTerminalPUnit.hom_ext _ _)

Premises used: CategoryTheory.Limits.IsTerminal.from, Profinite.exists_lift_of_finite_of_mono_of_epi, CategoryTheory.Limits.IsTerminal.hom_ext, CompHausLike.isTerminalPUnit
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : Profinite
inst : Nonempty.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_1 : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
this :
  ∀ (T : Profinite.{u})
    [Nonempty.{u + 1} (↑(T.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)],
    IsSplitEpi (Y := CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
      (IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) T)
k : Y ⟶ S
left :
  Eq (α := Y ⟶ CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
    (k ≫
      IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) S)
    (IsTerminal.from
      (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) Y)
h2 : f ≫ k = g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
⟨k, h2⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : Profinite
inst : Nonempty.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_1 : Finite.{u + 1} (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
this :
  ∀ (T : Profinite.{u})
    [Nonempty.{u + 1} (↑(T.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)],
    IsSplitEpi (Y := CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
      (IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) T)
k : Y ⟶ S
left :
  Eq (α := Y ⟶ CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})
    (k ≫
      IsTerminal.from
        (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) S)
    (IsTerminal.from
      (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) Y)
h2 : f ≫ k = g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
exact ⟨k, h2⟩
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
⊢ ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)

Tactic:
have (n : ℕ) : Finite <| lightToProfinite.obj (S.component n) :=
      inferInstanceAs (Finite (FintypeCat.toLightProfinite.obj _))