-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem liftOnWellOrder_type {δ : Sort v} (f : ∀ (α) [LinearOrder α] [WellFoundedLT α], δ)
    (c : ∀ (α) [LinearOrder α] [WellFoundedLT α] (β) [LinearOrder β] [WellFoundedLT β],
      typeLT α = typeLT β → f α = f β) {γ} [LinearOrder γ] [WellFoundedLT γ] :
    liftOnWellOrder (typeLT γ) f c = f γ

Proof state:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ ⟦{ α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }⟧.liftOn' (fun w => f w.α) ⋯ = f γ

Tactic:
rw [Quotient.liftOn'_mk]

Result:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ f { α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }.α = f γ

Proof state:
case h.e_2.h
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ linearOrderOfSTO { α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }.r = inst✝¹

Tactic:
exact LinearOrder.ext_lt fun _ _ ↦ Iff.rfl

Result:
no goals

Proof state:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ (type fun x1 x2 => x1 < x2).liftOnWellOrder f c = f γ

Tactic:
change Quotient.liftOn' ⟦_⟧ _ _ = _

Result:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ ⟦{ α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }⟧.liftOn' (fun w => f w.α) ⋯ = f γ

Proof state:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ f { α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }.α = f γ

Tactic:
congr

Result:
case h.e_2.h
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [inst : WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], ((type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2) → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ linearOrderOfSTO { α := γ, r := fun x1 x2 => x1 < x2, wo := ⋯ }.r = inst✝¹