[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (Finsupp.Lex r s) x
[PROOFSTEP]
rw [lex_eq_invImage_dfinsupp_lex]
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x
[PROOFSTEP]
classical
refine' InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
simpa only [toDFinsupp_support] using h
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x
[PROOFSTEP]
refine' InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
[GOAL]
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ (a : α), a ∈ x.support → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) a
⊢ ∀ (i : α), i ∈ DFinsupp.support (toDFinsupp x) → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i
[PROOFSTEP]
simpa only [toDFinsupp_support] using h
