-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩

Proof state:
case intro.intro.h.left.a
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
a₁✝ : α
b₁✝ : β a₁✝
a✝ : r a₁✝ xa
⊢ r a₁✝ xa

Tactic:
assumption

Result:
no goals

Proof state:
case intro.intro.h.right
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
b₁✝ : β xa
a✝ : s xa b₁✝ xb
⊢ Acc (Lex r s) ⟨xa, b₁✝⟩

Tactic:
apply ihb

Result:
case intro.intro.h.right.a
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
b₁✝ : β xa
a✝ : s xa b₁✝ xb
⊢ s xa b₁✝ xb

Proof state:
case intro
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b : β xa
⊢ Acc (Lex r s) ⟨xa, b⟩

Tactic:
induction (WellFounded.apply (acb xa) b) with
| intro xb _ ihb =>
  apply Acc.intro
  intro p lt
  cases lt with
  | left  => apply iha; assumption
  | right => apply ihb; assumption

Result:
no goals

Proof state:
case intro.intro.h.left
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
a₁✝ : α
b₁✝ : β a₁✝
a✝ : r a₁✝ xa
⊢ Acc (Lex r s) ⟨a₁✝, b₁✝⟩

Tactic:
apply iha

Result:
case intro.intro.h.left.a
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
a₁✝ : α
b₁✝ : β a₁✝
a✝ : r a₁✝ xa
⊢ r a₁✝ xa

Proof state:
case intro.intro
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
⊢ Acc (Lex r s) ⟨xa, xb⟩

Tactic:
apply Acc.intro

Result:
case intro.intro.h
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
⊢ ∀ (y : PSigma β), Lex r s y ⟨xa, xb⟩ → Acc (Lex r s) y

Proof state:
case intro.intro.h
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
p : PSigma β
lt : Lex r s p ⟨xa, xb⟩
⊢ Acc (Lex r s) p

Tactic:
cases lt with
| left  => apply iha; assumption
| right => apply ihb; assumption

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
aca : Acc r a
acb : ∀ (a : α), WellFounded (s a)
b : β a
⊢ Acc (Lex r s) ⟨a, b⟩

Tactic:
induction aca with
| intro xa _ iha =>
  induction (WellFounded.apply (acb xa) b) with
  | intro xb _ ihb =>
    apply Acc.intro
    intro p lt
    cases lt with
    | left  => apply iha; assumption
    | right => apply ihb; assumption

Result:
no goals

Proof state:
case intro.intro.h.right.a
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
b₁✝ : β xa
a✝ : s xa b₁✝ xb
⊢ s xa b₁✝ xb

Tactic:
assumption

Result:
no goals

Proof state:
case intro.intro.h
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
⊢ ∀ (y : PSigma β), Lex r s y ⟨xa, xb⟩ → Acc (Lex r s) y

Tactic:
intro p lt

Result:
case intro.intro.h
α : Sort u
β : α → Sort v
r : α → α → Prop
s : (a : α) → β a → β a → Prop
a : α
acb : ∀ (a : α), WellFounded (s a)
xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩
b xb : β xa
h✝ : ∀ (y : β xa), s xa y xb → Acc (s xa) y
ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩
p : PSigma β
lt : Lex r s p ⟨xa, xb⟩
⊢ Acc (Lex r s) p