awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.EffectiveEpi (goal)
Goal:
⊢ Preregular LightProfinite
have hs : ∀
  ⦃X Y :
    CompHausLike fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)⦄
  (f : X ⟶ Y),
  EffectiveEpi f →
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        X)
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            f) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              X) →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            Y)
Tactic: apply CompHausLike.preregular
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (goal)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c).Initial
have rw : (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial
Tactic: rw [initial_iff_comp_equivalence _ (StructuredArrow.post _ _ lightToProfinite)]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial
have this : ∀ (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)))
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functorOp c).Final
have this : (functor c).Initial
Tactic: have := functor_initial c hc
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : (functor c).Initial
⊢ (functorOp c).Final
have this₁ : IsEquivalence (C := (StructuredArrow c.pt toLightProfinite)ᵒᵖ)
  (StructuredArrow.toCostructuredArrow toLightProfinite c.pt)
Tactic: have : ((StructuredArrow.toCostructuredArrow toLightProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
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)
⊢ (functorOp c).Final
have this₁ : (functor c).rightOp.Final
Tactic: have : (functor c).rightOp.Final :=
    inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
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
⊢ 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)
have this : toLightProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right
Tactic: have := f.w
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Extend (hypothesis)
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
⊢ 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)
have this₁ : (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
Cleared hypotheses: this
-- 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
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have this : Finite T
Tactic: have : Finite T := Finite.of_surjective f' f'_surj
-- 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}
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have Z_closed : ∀ (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)
-- 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)
⊢ PairwiseDisjoint univ Z
have rw : ∀ ⦃i : S⦄,
  Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (Z i ∩ Z j).Nonempty → i = j
Tactic: rw [Set.pairwiseDisjoint_iff]
-- 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)
⊢ ∀ ⦃i : S⦄,
    Membership.mem (γ := Set S) univ i → ∀ ⦃j : S⦄, Membership.mem (γ := Set S) univ j → (Z i ∩ Z j).Nonempty → i = j
have 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
Tactic: simp only [image_inter_nonempty_iff, Z]
-- 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)
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)
⊢ g w = g w_1
have rw : g w = g w
Tactic: rw [f_inj hy]
-- 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)
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have Z_disj : 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]
-- 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}
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have D_clopen : ∀ (i : S), IsClopen (D i)
Tactic: have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg'
-- 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)
i : S
z : Y
hz : z ∈ Z i
⊢ z ∈ D i
have rw : g' z = f' i
Tactic: rw [mem_preimage, mem_singleton_iff]
-- 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)
i : S
z : Y
hz : z ∈ Z i
⊢ g' z = f' i
have obtain : ∀ x ∈ g ⁻¹' {i}, f x = z → g' z = f' i
Tactic: obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz
-- 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)
i : S
z : Y
hz : z ∈ Z i
x : X
left : x ∈ g ⁻¹' {i}
right : f x = z
⊢ g' z = f' i
have h_comm' : g' (f x) = f' (g x)
Tactic: have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm x
-- 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)
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have Z_subset_D : ∀ (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
-- 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
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have 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
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
-- 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
y : Y
h : Membership.mem (γ := Set Y) univ y
⊢ Membership.mem (γ := Set Y) (⋃ (i : S), D i) y
have simp : ∃ (i : S), y ∈ D i
Tactic: simp only [mem_iUnion]
-- 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
y : Y
h : Membership.mem (γ := Set Y) univ y
⊢ ∃ (i : S), y ∈ D i
have obtain : ∀ (s : S) (hs : f' s = g' y), ∃ (i : S), y ∈ D i
Tactic: obtain ⟨s, hs⟩ := f'_surj (g' 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
⊢ ∃ (k : Y → S), Continuous[inst_2, inst_6] k ∧ f' ∘ k = g' ∧ k ∘ f = g
have D_cover_univ : 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