-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
inr :
  d.lift i hj
      (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
        Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
          (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
        (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯) =
    d.lift i hi
      (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
        Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
          (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
        (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            (d.lift i hj
              (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
                Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
                  (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F))
                  x)
                (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)))
        ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (op i))) : (a : F.obj (op i)) → F.obj (op i))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) =
    d.lift i hi
      (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
        Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
          (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
        (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            (d.lift i hj
              (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
                Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
                  (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F))
                  x)
                (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)))
        ⋯)

Tactic:
rw [map_id, id_apply]

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id