[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ (invImage (fun a => PSigma.casesOn a fun ts snd => (length ts + length snd, length ts))
        Prod.instWellFoundedRelationProd).1
    { fst := ts, snd := t :: is } { fst := t :: ts, snd := is }
[PROOFSTEP]
simp_wf
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length ts + succ (length is), length ts)
    (succ (length ts) + length is, succ (length ts))
[PROOFSTEP]
simp [Nat.succ_add]
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length ts + succ (length is), length ts)
    (succ (length ts + length is), succ (length ts))
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ (invImage (fun a => PSigma.casesOn a fun ts snd => (length ts + length snd, length ts))
        Prod.instWellFoundedRelationProd).1
    { fst := is, snd := [] } { fst := t :: ts, snd := is }
[PROOFSTEP]
simp_wf
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length is, length is)
    (succ (length ts) + length is, succ (length ts))
[PROOFSTEP]
simp [Nat.succ_add]
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length is, length is)
    (succ (length ts + length is), succ (length ts))
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
l : List α
⊢ Decidable (Chain R a l)
[PROOFSTEP]
induction l generalizing a with
| nil => simp only [List.Chain.nil]; infer_instance
| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
l : List α
⊢ Decidable (Chain R a l)
[PROOFSTEP]
induction l generalizing a with
| nil => simp only [List.Chain.nil]; infer_instance
| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable (Chain R a [])
[PROOFSTEP]

| nil => simp only [List.Chain.nil]; infer_instance
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable (Chain R a [])
[PROOFSTEP]
simp only [List.Chain.nil]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]

| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]
haveI := ih
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
this : (a : α) → Decidable (Chain R a as)
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]
simp only [List.chain_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
this : (a : α) → Decidable (Chain R a as)
⊢ Decidable (R a a✝ ∧ Chain R a✝ as)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
⊢ Decidable (Chain' R l)
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
⊢ Decidable (Chain' R [])
[PROOFSTEP]
dsimp only [List.Chain']
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
head✝ : α
tail✝ : List α
⊢ Decidable (Chain' R (head✝ :: tail✝))
[PROOFSTEP]
dsimp only [List.Chain']
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
head✝ : α
tail✝ : List α
⊢ Decidable (Chain R head✝ tail✝)
[PROOFSTEP]
infer_instance
