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

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

Tactic:
apply Acc.intro

Result:
case intro.intro.h
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝¹ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → Acc (RevLex r s) ⟨y, xb⟩
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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

Tactic:
apply iha

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

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

Tactic:
induction acb with
| intro xb _ ihb =>
  intro a
  induction (aca a) with
  | intro xa _ iha =>
    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.a
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝¹ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → Acc (RevLex r s) ⟨y, xb⟩
a₁✝ : α
a✝ : r a₁✝ xa
⊢ r a₁✝ xa

Tactic:
assumption

Result:
no goals

Proof state:
case intro.intro.h
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝¹ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → Acc (RevLex r s) ⟨y, xb⟩
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro p lt

Result:
case intro.intro.h
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝¹ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → Acc (RevLex r s) ⟨y, xb⟩
p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
lt : RevLex r s p ⟨xa, xb⟩
⊢ Acc (RevLex r s) p

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

Tactic:
apply ihb

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

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

Tactic:
assumption

Result:
no goals

Proof state:
case intro
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
⊢ ∀ (a : α), Acc (RevLex r s) ⟨a, xb⟩

Tactic:
intro a

Result:
case intro
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a : α
⊢ Acc (RevLex r s) ⟨a, xb⟩

Proof state:
case intro
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a : α
⊢ Acc (RevLex r s) ⟨a, xb⟩

Tactic:
induction (aca a) with
| intro xa _ iha =>
  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
α : Sort u
β : Sort v
r : α → α → Prop
s : β → β → Prop
b : β
aca : ∀ (a : α), Acc r a
xb : β
h✝¹ : ∀ (y : β), s y xb → Acc s y
ihb : ∀ (y : β), s y xb → ∀ (a : α), Acc (RevLex r s) ⟨a, y⟩
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha : ∀ (y : α), r y xa → Acc (RevLex r s) ⟨y, xb⟩
p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
lt : RevLex r s p ⟨xa, xb⟩
⊢ Acc (RevLex r s) p

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

Result:
no goals