-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b)

Proof state:
case intro.intro.right
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
b₁✝ : β
h : rb b₁✝ xb
⊢ Acc (Prod.Lex ra rb) { fst := xa, snd := b₁✝ }

Tactic:
apply ihb _ h

Result:
no goals

Proof state:
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
aca : Acc ra a
acb : ∀ (b : β), Acc rb b
b : β
⊢ Acc (Prod.Lex ra rb) { fst := a, snd := b }

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

Result:
no goals

Proof state:
case intro.intro.left
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
a₁✝ : α
b₁✝ : β
h : ra a₁✝ xa
⊢ Acc (Prod.Lex ra rb) { fst := a₁✝, snd := b₁✝ }

Tactic:
apply iha _ h

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
p : α × β
lt : Prod.Lex ra rb p { fst := xa, snd := xb }
⊢ Acc (Prod.Lex ra rb) p

Tactic:
cases lt with
| left  _ _ h => apply iha _ h
| right _ h   => apply ihb _ h

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
⊢ ∀ (y : α × β), Prod.Lex ra rb y { fst := xa, snd := xb } → Acc (Prod.Lex ra rb) y

Tactic:
intro p lt

Result:
case intro.intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
p : α × β
lt : Prod.Lex ra rb p { fst := xa, snd := xb }
⊢ Acc (Prod.Lex ra rb) p

Proof state:
case intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b : β
⊢ Acc (Prod.Lex ra rb) { fst := xa, snd := b }

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

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
⊢ Acc (Prod.Lex ra rb) { fst := xa, snd := xb }

Tactic:
apply Acc.intro (xa, xb)

Result:
case intro.intro
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
a : α
acb : ∀ (b : β), Acc rb b
xa : α
h✝¹ : ∀ (y : α), ra y xa → Acc ra y
iha : ∀ (y : α), ra y xa → ∀ (b : β), Acc (Prod.Lex ra rb) { fst := y, snd := b }
b xb : β
h✝ : ∀ (y : β), rb y xb → Acc rb y
ihb : ∀ (y : β), rb y xb → Acc (Prod.Lex ra rb) { fst := xa, snd := y }
⊢ ∀ (y : α × β), Prod.Lex ra rb y { fst := xa, snd := xb } → Acc (Prod.Lex ra rb) y