-- Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean
lemma val_injective {j : J} {e e' : d.Extension val₀ j} (h : e.val = e'.val) : e = e'

Proof state:
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
e e' : d.Extension val₀ j
h : e.val = e'.val
⊢ e = e'

Tactic:
cases e

Result:
case 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
e' : d.Extension val₀ j
val✝ : F.obj (op j)
map_zero✝ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝,
          ⋯⟩
h : { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val = e'.val
⊢ { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ } = e'

Proof state:
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✝¹ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝¹ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝,
          ⋯⟩
map_zero✝ :
  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),
    F.map (homOfLE ⋯).op { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.succ i ⋯
        (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),
    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⟩ =>
            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✝ }

Tactic:
rfl

Result:
no goals

Proof state:
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✝¹ : F.map (homOfLE ⋯).op val✝¹ = val₀
map_succ✝¹ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝¹ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝¹)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝¹ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝¹,
          ⋯⟩
val✝ : F.obj (op j)
map_zero✝ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => 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

Result:
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✝¹ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝¹ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝,
          ⋯⟩
map_zero✝ :
  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),
    F.map (homOfLE ⋯).op { val := val✝, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
      d.succ i ⋯
        (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),
    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⟩ =>
            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✝ }