awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
⊢ f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone = g
have hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
Tactic: have hg : g = (isLimitOfPreserves _ S.asLimit).lift (k_cone.extend f) := by
      apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)
      intro n
      simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
⊢ f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone = g
have rw : f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone =
  (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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 : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
⊢ ∃ (h : Y ⟶ S), f ≫ h = g
have obtain : ∀ (h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S),
  lightToProfinite.map f ≫ h = lightToProfinite.map g → ∃ (h : Y ⟶ S), f ≫ h = g
Tactic: obtain ⟨h, _⟩ := Injective.factors (lightToProfinite.map g) (lightToProfinite.map f)
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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 : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h_1 : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h_2 : lightToProfinite.map f ≫ h = lightToProfinite.map g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g
have refine : f ≫ lightToProfiniteFullyFaithful.preimage h = g
Tactic: refine ⟨lightToProfiniteFullyFaithful.preimage h, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Injective (goal)
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 : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h_1 : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h_2 : lightToProfinite.map f ≫ h = lightToProfinite.map g
⊢ f ≫ lightToProfiniteFullyFaithful.preimage h = g
have apply : lightToProfinite.map (f ≫ lightToProfiniteFullyFaithful.preimage h) = lightToProfinite.map g
Tactic: apply lightToProfiniteFullyFaithful.map_injective
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (goal)
Goal:
⊢ IsClosedEmbedding (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
have refine_1 : Function.Injective (α := OnePoint ℕ) (β := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
Tactic: refine .of_continuous_injective_isClosedMap
    natUnionInftyEmbedding.continuous ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (goal)
Goal:
refine_1 : Function.Injective (α := OnePoint ℕ) (β := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
⊢ IsClosedEmbedding (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
have refine_2 : IsClosedMap (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
Tactic: refine .of_continuous_injective_isClosedMap
    natUnionInftyEmbedding.continuous ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (hypothesis)
Goal:
m : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some m) : ℝ)
⊢ none = Option.some m
have h₁ : 0 = HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, zero_eq_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (goal)
Goal:
m : ℕ
h : 0 = HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ none = Option.some m
have refine_1 : ∀ (h : False), False
Tactic: assumption_mod_cast
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (hypothesis)
Goal:
n : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some n) : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
⊢ Option.some n = none
have h₁ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 0
Tactic: simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (goal)
Goal:
n : ℕ
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 0
⊢ Option.some n = none
have refine_1 : ∀ (h : False), False
Tactic: assumption_mod_cast
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (hypothesis)
Goal:
n m : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some n) : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some m) : ℝ)
⊢ Option.some n = Option.some m
have h₁ : n = m
Tactic: simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.Sequence (goal)
Goal:
n m : ℕ
h : n = m
⊢ Option.some n = Option.some m
have refine_1 : Option.some m = Option.some m
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.AsLimit (goal)
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
⊢ ∃ (a_1 :
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X.asLimitCone.pt),
    (ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
            X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X.asLimitCone.pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone X.diagram).pt)
        a_1 =
      a
have h : (ConcreteCategory.hom (FC :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
          (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
        (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
        X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            X.asLimitCone.pt) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
          (limitCone X.diagram).pt)
    b =
  a
Tactic: use b
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.AsLimit (goal)
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
⊢ (ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
          X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              X.asLimitCone.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            (limitCone X.diagram).pt)
      b =
    a
have h : (↑((ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
            X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X.asLimitCone.pt) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (limitCone X.diagram).pt)
        b) :
    (j : DiscreteQuotient (↑X.toTop : Type u)) →
      (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) =
  (↑a :
    (j : DiscreteQuotient (↑X.toTop : Type u)) →
      (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Profinite
⊢ TotallyDisconnectedSpace
    (↑((CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).pt.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))
have change : TotallyDisconnectedSpace
  (↑{u :
        (j : J) →
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v)) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  TopCat.carrier) (((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) :
                (a : (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj i) : Type (max u v))) →
                  (↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type (max u v)))
              (u i) =
            u j} :
    Type (max u v))
Tactic: change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Profinite
S : Limits.Cone F
x : S.pt ⟶ (limitCone.{v, u} F).pt
h : ∀ (j : J), x ≫ (limitCone.{v, u} F).π.app j = S.π.app j
j : J
⊢ profiniteToCompHaus.map x ≫ (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app j =
    (profiniteToCompHaus.mapCone S).π.app j
have simp : Eq (α := profiniteToCompHaus.obj S.pt ⟶ profiniteToCompHaus.obj (F.obj j))
  (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
      C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
        (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
      (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
      (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (TopCat.Hom.hom x.hom) ≫
    (CompHaus.limitCone.{v, u} (F ⋙ profiniteToCompHaus)).π.app j)
  (ConcreteCategory.ofHom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    (TopCat.Hom.hom (x ≫ (limitCone.{v, u} F).π.app j).hom))
Tactic: simp [← h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Basic (goal)
Goal:
X Y : Profinite
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y)
have mp : Epi f →
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Basic (goal)
Goal:
X Y : Profinite
f : X ⟶ Y
⊢ Epi f →
    ∀ (b : (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      ∃ (a : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        (ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f :
              (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
            a =
          b
have mp : (∃ (b : (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      (ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f :
            (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
          a ≠
        b) →
  ¬Epi f
Tactic: contrapose!