awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)

Tactic:
have : ∀ i, Epi ((lightToProfinite.mapCone c).π.app i) :=
    fun i ↦ inferInstanceAs (Epi (lightToProfinite.map (c.π.app i)))
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Tactic:
Profinite.Extend.functor_initial _ (isLimitOfPreserves lightToProfinite hc)

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Functor.comp, FintypeCat.toProfinite, CategoryTheory.StructuredArrow.mk, lightToProfinite, CategoryTheory.Limits.isLimitOfPreserves, Profinite.Extend.functor_initial, Profinite.Extend.functor
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Tactic:
exact Profinite.Extend.functor_initial _ (isLimitOfPreserves lightToProfinite hc)

Premises used: lightToProfinite, CategoryTheory.Limits.isLimitOfPreserves, Profinite.Extend.functor_initial
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c).Initial

Tactic:
have := functor_initial c hc
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : (functor c).Initial
⊢ IsEquivalence (C := (StructuredArrow c.pt toLightProfinite)ᵒᵖ)
    (StructuredArrow.toCostructuredArrow toLightProfinite c.pt)

Tactic:
have : ((StructuredArrow.toCostructuredArrow toLightProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this_1 : (functor c).Initial
this :
  IsEquivalence (C := (StructuredArrow c.pt toLightProfinite)ᵒᵖ)
    (StructuredArrow.toCostructuredArrow toLightProfinite c.pt)
⊢ (functor c).rightOp.Final

Tactic:
have : (functor c).rightOp.Final :=
    inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this_1 : (functor c).Initial
this_2 :
  IsEquivalence (C := (StructuredArrow c.pt toLightProfinite)ᵒᵖ)
    (StructuredArrow.toCostructuredArrow toLightProfinite c.pt)
this : (functor c).rightOp.Final
⊢ (functorOp c).Final

Tactic:
Functor.final_comp (functor c).rightOp _

Premises used: LightProfinite.Extend.functor, CategoryTheory.Functor.final_comp, CategoryTheory.Functor.rightOp, LightProfinite.Extend.functorOp
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this_1 : (functor c).Initial
this_2 :
  IsEquivalence (C := (StructuredArrow c.pt toLightProfinite)ᵒᵖ)
    (StructuredArrow.toCostructuredArrow toLightProfinite c.pt)
this : (functor c).rightOp.Final
⊢ (functorOp c).Final

Tactic:
exact Functor.final_comp (functor c).rightOp _

Premises used: LightProfinite.Extend.functor, CategoryTheory.Functor.final_comp, CategoryTheory.Functor.rightOp
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} LightProfinite C
S : LightProfinite
x x_1 : StructuredArrow S toLightProfinite
f : x ⟶ x_1
⊢ CategoryTheory.Functor.map (obj (const (StructuredArrow S toLightProfinite)) (G.obj S)) f ≫ G.map x_1.hom =
    G.map x.hom ≫ (StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G).map f

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfinite C
⊢ G.mapCone c = Cone.whisker (functor c) (cone G c.pt)

Tactic:
rfl

Premises used: LightProfinite.Extend.functor, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.StructuredArrow.mk, CategoryTheory.Limits.Cone.whisker, CategoryTheory.Functor.mapCone, rfl
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} LightProfiniteᵒᵖ C
S : LightProfinite
x x_1 : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x ⟶ x_1
⊢ toLightProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right

Tactic:
have := f.w
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} LightProfiniteᵒᵖ C
S : LightProfinite
x x_1 : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x ⟶ x_1
this : toLightProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right
⊢ (toLightProfinite.map f.left.unop).op ≫ x_1.hom = x.hom

Tactic:
simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.right_eq_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} LightProfiniteᵒᵖ C
S : LightProfinite
x x_1 : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x ⟶ x_1
this : (toLightProfinite.map f.left.unop).op ≫ x_1.hom = x.hom
⊢ Eq (α :=
    obj (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G) x ⟶
      obj.{u_2, v_1, u_2 + 1, u_1}
        (obj (const (CostructuredArrow toLightProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) x_1)
    (CategoryTheory.Functor.map (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G)
        f ≫
      G.map x_1.hom)
    (G.map x.hom ≫
      CategoryTheory.Functor.map
        (obj (const (CostructuredArrow toLightProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) f)

Tactic:
simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, const_obj_obj, Functor.comp_map,
        CostructuredArrow.proj_map, op_map, ← map_comp, this, const_obj_map, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CostructuredArrow.proj_obj, CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.proj_map, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.comp_map, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ C
⊢ G.mapCocone c.op = Cocone.whisker (Equivalence.functor (opOpEquivalence ℕ) ⋙ functorOp c) (cocone G c.pt)

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.mapCocone, Quiver.Hom.op, CategoryTheory.Functor.comp, Quiver.Hom.unop, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.Topology.Category.LightProfinite.Extend
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
S : LightProfinite
i : ℕᵒᵖ
⊢ Epi (S.asLimitCone.π.app i)

Tactic:
(epi_iff_surjective _).mpr (S.proj_surjective _)

Premises used: Iff.mpr, LightProfinite.epi_iff_surjective, LightProfinite.proj_surjective
-- 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
⊢ Finite T

Tactic:
have : Finite T := Finite.of_surjective f' f'_surj
-- 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}
⊢ ∀ (i : S), IsClosed[inst_2] (Z i)

Tactic:
have Z_closed (i) : IsClosed (Z i) :=
    (IsClosedEmbedding.isClosed_iff_image_isClosed (Continuous.isClosedEmbedding hf f_inj)).mp
    (IsClosed.preimage hg isClosed_singleton)
-- 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)
rw :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (Z i ∩ Z j).Nonempty → i = j
⊢ PairwiseDisjoint univ Z

Tactic:
rw [Set.pairwiseDisjoint_iff]

Premises used: Set.pairwiseDisjoint_iff
-- 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)
simp :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i →
      ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (g ⁻¹' {i} ∩ f ⁻¹' f '' g ⁻¹' {j}).Nonempty → i = j
⊢ ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (Z i ∩ Z j).Nonempty → i = j

Tactic:
simp only [image_inter_nonempty_iff, Z]

Premises used: Set.image_inter_nonempty_iff
-- 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)
w : X
h : Membership.mem (γ := Set S) univ (g w)
w_1 : X
hy : f w_1 = f w
h_1 : Membership.mem (γ := Set S) univ (g w_1)
rw rw₁ : g w = g w
⊢ g w = g w_1

Tactic:
rw [f_inj hy]
-- 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)
⊢ PairwiseDisjoint univ Z

Tactic:
have Z_disj : univ.PairwiseDisjoint Z := by
    rw [Set.pairwiseDisjoint_iff]
    simp only [image_inter_nonempty_iff, Z]
    rintro _ _ _ _ ⟨_, rfl, ⟨_, rfl, hy⟩⟩
    rw [f_inj hy]
-- 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}
⊢ ∀ (i : S), IsClopen (D i)

Tactic:
have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg'
-- 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)
i : S
z : Y
hz : z ∈ Z i
rw : g' z = f' i
⊢ z ∈ D i

Tactic:
rw [mem_preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- 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)
i : S
z : Y
hz : z ∈ Z i
obtain : ∀ x ∈ g ⁻¹' {i}, f x = z → g' z = f' i
⊢ g' z = f' i

Tactic:
obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz

Premises used: Set.mem_image, 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)
i : S
z : Y
hz : z ∈ Z i
x : X
left : x ∈ g ⁻¹' {i}
right : f x = z
⊢ g' (f x) = f' (g x)

Tactic:
have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm 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)
i : S
z : Y
hz : z ∈ Z i
x : X
left : x ∈ g ⁻¹' {i}
right : f x = z
h_comm' : g' (f x) = f' (g x)
⊢ g' z = f' i

Tactic:
simp_all
-- 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)
⊢ ∀ (i : S), Z i ⊆ D i

Tactic:
have Z_subset_D i : Z i ⊆ D i := by
    intro z hz
    rw [mem_preimage, mem_singleton_iff]
    obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz
    have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm x
    simp_all
-- 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
obtain :
  ∀ (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), ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
obtain ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ :=
    exists_clopen_partition_of_clopen_cover Z_closed D_clopen Z_subset_D Z_disj

Premises used: exists_clopen_partition_of_clopen_cover
-- 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
y : Y
_ : Membership.mem (γ := Set Y) univ y → Membership.mem (γ := Set Y) (⋃ (i : S), D i) y
⊢ Membership.mem (γ := Set Y) univ y → Membership.mem (γ := Set Y) (⋃ (i : S), D i) y

Tactic:
_
-- 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
y : Y
h : Membership.mem (γ := Set Y) univ y
simp : ∃ (i : S), y ∈ D i
⊢ Membership.mem (γ := Set Y) (⋃ (i : S), D i) y

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion