awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (hypothesis)
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)
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have C_cover_univ : 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)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
have 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
Tactic: rw [Set.pairwiseDisjoint_iff] at C_disj
Cleared hypotheses: C_disj, D_cover_univ, C_cover_univ, i, j, x, hxi, hxj
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (hypothesis)
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
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have h_glue : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
have refine_1 : IsLocallyConstant (Y := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ)
Tactic: refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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)
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have refine_2 : f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ = g'
Tactic: refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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'
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have refine_3 : liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f = g
Tactic: refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
⊢ IsLocallyConstant (Y := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ)
have 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})
Tactic: rw [IsLocallyConstant.iff_isOpen_fiber]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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] (preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s})
have h : preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s} = C s
Tactic: convert! (C_clopen s).2
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
⊢ preimage (β := S) (liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) {s} = C s
have 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
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
⊢ f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ = g'
have 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
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (hypothesis)
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
⊢ (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y
have hy : Membership.mem (γ := Set Y) (⋃ (i : S), C i) y
Tactic: have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
⊢ (f' ∘ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ) y = g' y
have 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
Tactic: obtain ⟨i, hi⟩ := mem_iUnion.mp hy
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
⊢ liftCover C (fun (i : S) (x : (↑(C i) : Type u_2)) ↦ i) h_glue C_cover_univ ∘ f = g
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (hypothesis)
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
⊢ ∃ (h : Y ⟶ S), f ≫ h = g
have 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)
Tactic: have (T : Profinite.{u}) [Nonempty T] : IsSplitEpi (CompHausLike.isTerminalPUnit.from T) :=
      IsSplitEpi.mk' { section_ := CompHausLike.const _ (Nonempty.some inferInstance) }
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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)
⊢ ∃ (h : Y ⟶ S), f ≫ h = g
have 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
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 _ _)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (hypothesis)
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
⊢ ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have this : ∀ (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 _))