-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lt_wf : @WellFounded Cardinal.{u} (· < ·) :=
  ⟨fun a =>
    by_contradiction fun h => by
      let ι := { c : Cardinal // ¬Acc (· < ·) c }
      let f : ι → Cardinal := Subtype.val
      haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
      obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out
      refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)
      have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
      simpa only [mk_out] using this⟩

Proof state:
case intro.mk.intro
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 => x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
⊢ False

Tactic:
refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)

Result:
case intro.mk.intro
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 => x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 => x1 < x2) j
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Proof state:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (?u.56390 + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{?u.56390} := Subtype.val
⊢ False

Tactic:
haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩

Result:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
⊢ False

Proof state:
case intro.mk.intro
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 => x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 => x1 < x2) j
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Tactic:
have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩

Result:
case intro.mk.intro
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 => x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 => x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Proof state:
case intro.mk.intro
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 => x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 => x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Tactic:
simpa only [mk_out] using this

Result:
no goals

Proof state:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (?u.56390 + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
⊢ False

Tactic:
let f : ι → Cardinal := Subtype.val

Result:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 => x1 < x2) a
ι : Type (max 0 (?u.56390 + 1)) := { c // ¬Acc (fun x1 x2 => x1 < x2) c }
f : ι → Cardinal.{?u.56390} := Subtype.val
⊢ False