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 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
⊢ ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have this₁ : Nonempty.{u + 1}
  (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
Tactic: have : Nonempty <| lightToProfinite.obj (S.component 0) :=
      Nonempty.map (S.proj 0) inferInstance
-- 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 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
⊢ ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have this₁ : ∀ (n : ℕ), Epi (S.transitionMap n)
Tactic: have (n : ℕ) : Epi (S.transitionMap n) := (LightProfinite.epi_iff_surjective _).mpr
      (S.surjective_transitionMap n)
-- 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)
⊢ ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have obtain : ∀ (k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0)))
  (h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)), ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
Tactic: obtain ⟨k0, h_down0⟩ := Injective.factors (g ≫ lightToProfinite.map (S.proj 0)) 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 : 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)
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)
have rw : g ≫ lightToProfinite.map (S.proj n) =
  g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
Tactic: rw [h_down, ← Functor.map_comp, ← S.proj_comp_transitionMap n]
-- 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)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
rw :
  g ≫ lightToProfinite.map (S.proj n) =
    g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
⊢ f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
have rw₁ : g ≫ lightToProfinite.map (S.proj n) = g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)
Tactic: rw [h_down, ← Functor.map_comp, ← S.proj_comp_transitionMap n]
-- 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)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
rw :
  g ≫ lightToProfinite.map (S.proj n) =
    g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
rw₁ : g ≫ lightToProfinite.map (S.proj n) = g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)
⊢ f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
have rw₂ : g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE sorry))) =
  g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)
Tactic: rw [h_down, ← Functor.map_comp, ← S.proj_comp_transitionMap n]
-- 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 : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have 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)
Tactic: have 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) := by
      rw [h_down, ← Functor.map_comp, ← S.proj_comp_transitionMap n]
-- 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 : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have 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))
Tactic: have 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)) :=
      exists_lift_of_finite_of_mono_of_epi f (lightToProfinite.map (S.transitionMap n))
        (g ≫ lightToProfinite.map (S.proj (n + 1))) k (h_comm _ _ h_down)
-- 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 : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
Tactic: have h_down (n : ℕ) : f ≫ (k_seq n).val = g ≫ lightToProfinite.map (S.proj n) :=
      (k_seq n).prop
-- 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 : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have 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))
Tactic: have h_up : ∀ n, (k_seq (n + 1)).val ≫ lightToProfinite.map (S.transitionMap n) = (k_seq n).val
    | 0 => (h_step 0 k0 h_down0).choose_spec.1
    | n + 1 => (h_step (n + 1) (k_seq (n + 1)).val (k_seq (n + 1)).prop).choose_spec.1
-- 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))) ⋯ }
⊢ ∃ (h : Y ⟶ lightToProfinite.obj S), f ≫ h = g
have refine : f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone = g
Tactic: refine ⟨(isLimitOfPreserves _ S.asLimit).lift k_cone, ?_⟩
-- 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))) ⋯ }
⊢ g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
have x : ∀ (j : ℕᵒᵖ), g ≫ (lightToProfinite.mapCone S.asLimitCone).π.app j = (k_cone.extend f).π.app j
Tactic: apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)