-- 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 =
    (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
have x : ∀ (j : ℕᵒᵖ),
  (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫ (lightToProfinite.mapCone S.asLimitCone).π.app j =
    (k_cone.extend f).π.app j
Tactic: apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)