Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by
    -- help the instance inference a bit
    have (n : ℕ) : Finite <| lightToProfinite.obj (S.component n) :=
      inferInstanceAs (Finite (FintypeCat.toLightProfinite.obj _))
    have : Nonempty <| lightToProfinite.obj (S.component 0) :=
      Nonempty.map (S.proj 0) inferInstance
    have (n : ℕ) : Epi (S.transitionMap n) := (LightProfinite.epi_iff_surjective _).mpr
      (S.surjective_transitionMap n)
    -- base step of the induction: find k0 : Y ⟶ S.component 0
    obtain ⟨k0, h_down0⟩ := Injective.factors (g ≫ lightToProfinite.map (S.proj 0)) f
    /- Induction step: `next` produces k n+1 out of k n:
    ```
    X        --f-->  Y
    |g' (n+1)        |k n
    v                v
    S (n+1) --p n-> S n
    ```
    find `k (n+1) : Y ⟶ S' (n+1)` making both diagrams commute. That is:
      - `h_up (n+1) : k (n+1) ≫ p n = k n`
      - `h_down n+1 : f ≫ k (n+1) = g' (n+1)`
    Construction of `k (n+1)` through extension lemma requires as input:
      - `h_comm n : g' (n+1) ≫ p n = f ≫ k n`, which can be obtained from h_down n. -/
    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]
    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)
    let lifts (n : ℕ) := { k : Y ⟶ lightToProfinite.obj (S.component n) //
      f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
    let next (n : ℕ) : lifts n → lifts (n + 1) :=
      fun k ↦ ⟨(h_step n k.val k.property).choose, (h_step n k.val k.property).choose_spec.2⟩
    -- now define a sequence of lifts using induction
    let k_seq (n : Nat) : lifts n := Nat.rec ⟨k0, h_down0⟩ next n
    -- `h_up` and `h_down` are the required commutativity properties
    have h_down (n : ℕ) : f ≫ (k_seq n).val = g ≫ lightToProfinite.map (S.proj n) :=
      (k_seq n).prop
    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
    let k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
      { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ (k_seq n).val) (fun n ↦ (h_up n).symm) }
    -- now the induced map `Y ⟶ S = limₙ Sₙ` is the desired map
    refine ⟨(isLimitOfPreserves _ S.asLimit).lift k_cone, ?_⟩
    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]
    rw [hg]
    apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)
    intro n
    simp [-Functor.mapCone_pt, -Functor.mapCone_π_app]

Goal state after: