-- Mathlib/CategoryTheory/Limits/Types.lean
/-- Auxiliary lemma. Use `limit_of_surjections_surjective` instead. -/
lemma surjective_π_app_zero_of_surjective_map_aux :
    Function.Surjective ((limitCone F).π.app ⟨0⟩)

Proof state:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m : ℕ
h : m ≤ n
⊢ F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op n)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)

Tactic:
induction h with
| refl =>
  erw [CategoryTheory.Functor.map_id, types_id_apply]
| @step p h ih =>
  rw [← ih]
  have h' : m ≤ p := h
  erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
    types_comp_apply, (hF p _).choose_spec]
  rfl

Result:
no goals

Proof state:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
⊢ (fun x =>
      match x with
      | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n) ∈
    F.sections

Tactic:
intro ⟨n⟩ ⟨m⟩ ⟨⟨⟨(h : m ≤ n)⟩⟩⟩

Result:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m : ℕ
h : m ≤ n
⊢ F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op n)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)

Proof state:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
⊢ Function.Surjective ((limitCone F).π.app (Opposite.op 0))

Tactic:
intro a

Result:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
⊢ ∃ a_1, (limitCone F).π.app (Opposite.op 0) a_1 = a

Proof state:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ F.map (homOfLE h').op (CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a p) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Tactic:
rfl

Result:
no goals

Proof state:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p.succ)) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Tactic:
have h' : m ≤ p := h

Result:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p.succ)) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Proof state:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p.succ)) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Tactic:
erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
  types_comp_apply, (hF p _).choose_spec]

Result:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ F.map (homOfLE h').op (CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a p) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Proof state:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
⊢ ∃ a_1, (limitCone F).π.app (Opposite.op 0) a_1 = a

Tactic:
refine ⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩

Result:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
⊢ (fun x =>
      match x with
      | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n) ∈
    F.sections