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
y : Y
h : Membership.mem (γ := Set Y) univ y
obtain : ∀ (s : S) (hs : f' s = g' y), ∃ (i : S), y ∈ D i
⊢ ∃ (i : S), y ∈ D i

Tactic:
obtain ⟨s, hs⟩ := f'_surj (g' 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
y : Y
h : Membership.mem (γ := Set Y) univ y
s : S
hs : f' s = g' y
⊢ ∃ (i : S), y ∈ D i

Tactic:
grind
-- 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
⊢ Subset.{u_2} (α := Set Y) univ (⋃ (i : S), D i)

Tactic:
have D_cover_univ : univ ⊆ (⋃ i, D i) := by
    intro y _
    simp only [mem_iUnion]
    obtain ⟨s, hs⟩ := f'_surj (g' y)
    grind
-- 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)
⊢ Eq.{u_2 + 1} (α := Set Y) (⋃ (i : S), C i) univ

Tactic:
have C_cover_univ : ⋃ i, C i = univ := univ_subset_iff.mp (subset_trans D_cover_univ C_cover_D)
-- 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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
rw :
  ∀
    (C_disj :
      ∀ ⦃i : S⦄,
        Membership.mem (γ := Set S) univ i →
          ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (C i ∩ C j).Nonempty → i = j)
    (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) (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j),
    i = j
⊢ i = j

Tactic:
rw [Set.pairwiseDisjoint_iff] at C_disj

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)
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 :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (C i ∩ C j).Nonempty → i = j
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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ Membership.mem (γ := Set S) univ i

Tactic:
simp
-- 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 :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (C i ∩ C j).Nonempty → i = j
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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ Membership.mem (γ := Set S) univ j

Tactic:
simp
-- 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 :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (C i ∩ C j).Nonempty → i = j
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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ x ∈ C i ∩ C j

Tactic:
grind
-- 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 :
  ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (C i ∩ C j).Nonempty → i = j
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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i = j

Tactic:
exact C_disj (by simp) (by simp) ⟨x, by grind⟩

Premises used: Exists.intro
-- 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
⊢ ∀ (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j), i = j

Tactic:
have h_glue (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : i = j := by
    rw [Set.pairwiseDisjoint_iff] at C_disj
    exact C_disj (by simp) (by simp) ⟨x, by grind⟩
-- 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
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩

Premises used: Set.liftCover, And.intro, Exists.intro, IsLocallyConstant.continuous
-- 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_1 : IsLocallyConstant (Y := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ)
refine_2 : f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ = g'
refine_3 : liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f = g
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩
-- 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_1 :
  ∀ (y : S),
    IsOpen[inst_2] (preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {y})
⊢ IsLocallyConstant (Y := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ)

Tactic:
rw [IsLocallyConstant.iff_isOpen_fiber]

Premises used: IsLocallyConstant.iff_isOpen_fiber
-- 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
⊢ IsOpen[inst_2] (C s)

Tactic:
(C_clopen s).2

Premises used: And.right
-- 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
h : preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s} = C s
⊢ IsOpen[inst_2] (preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s})

Tactic:
convert! (C_clopen s).2

Premises used: And.right
-- 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
h :
  ∀ (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
⊢ preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s} = C s

Tactic:
ext y