Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case mk.mk
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val✝¹ : F.obj (op j)
map_zero✝¹ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹ = val₀
map_succ✝¹ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹ =
      d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op)) val✝¹ =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝¹,
          ⋯⟩
val✝ : F.obj (op j)
map_zero✝ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = val₀
map_succ✝ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op)) val✝ =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝,
          ⋯⟩
h :
  { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val
⊢ { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ } =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }

Tactic:
subst h

Goal state after:
case mk.mk
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val✝ : F.obj (op j)
map_zero✝¹ : (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = val₀
map_succ✝¹ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op)) val✝ =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val✝,
          ⋯⟩
map_zero✝ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
    val₀
map_succ✝ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
        { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.succ i ⋯
        ((ConcreteCategory.hom (F.map (homOfLE ⋯).op))
          { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    (ConcreteCategory.hom (F.map (homOfLE hij).op))
        { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.lift i hi
        ⟨fun x ↦
          match x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
              { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val,
          ⋯⟩
⊢ { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ } =
    { val := { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val,
      map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }