α : 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
α : 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
rw [lex_eq_invImage_dfinsupp_lex]
no goals
α : 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
classical
  refine' InvImage.accessible toDfinsupp (Dfinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
  simpa only [toDfinsupp_support] using h
α : 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
α : 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
refine' InvImage.accessible toDfinsupp (Dfinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ _)
no goals
α : 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
simpa only [toDfinsupp_support] using h