case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (Dfinsupp.Lex r s) (single i a)
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i : ι
hi : Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i
⊢ ∀ (a : α i), Acc (Dfinsupp.Lex r s) (single i a)
induction' hi with i _ ih
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
⊢ (fun x => Acc (Dfinsupp.Lex r s) (single i x)) a
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (Dfinsupp.Lex r s) (single i a)
refine fun a => WellFounded.induction (hs i)
  (C := fun x ↦ Acc (Dfinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
⊢ Dfinsupp.Lex r s x (single i a) → Acc (Dfinsupp.Lex r s) x
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
⊢ (fun x => Acc (Dfinsupp.Lex r s) (single i x)) a
refine Acc.intro _ fun x ↦ ?_
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (↑(single i a) k)
⊢ Acc (Dfinsupp.Lex r s) x
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
⊢ Dfinsupp.Lex r s x (single i a) → Acc (Dfinsupp.Lex r s) x
rintro ⟨k, hr, hs⟩
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (if h : i = k then Eq.recOn h a else 0)
⊢ Acc (Dfinsupp.Lex r s) x
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (↑(single i a) k)
⊢ Acc (Dfinsupp.Lex r s) x
rw [single_apply] at hs
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (Dfinsupp.Lex r s) x

case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (Dfinsupp.Lex r s) x
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (if h : i = k then Eq.recOn h a else 0)
⊢ Acc (Dfinsupp.Lex r s) x
split_ifs at hs with hik
case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (Dfinsupp.Lex r s) x

case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (Dfinsupp.Lex r s) x
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (Dfinsupp.Lex r s) x

case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (Dfinsupp.Lex r s) x
swap
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
⊢ Acc (Dfinsupp.Lex r s) x
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (Dfinsupp.Lex r s) x
subst hik
no goals
case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (Dfinsupp.Lex r s) x
exact (hbot hs).elim
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
⊢ Acc (Dfinsupp.Lex r s) x
refine Lex.acc_of_single hbot x fun j hj ↦ ?_
case intro.intro.intro.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
hj : i ∈ support x
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single i (↑x i))

case intro.intro.intro.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
obtain rfl | hij := eq_or_ne i j
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))

case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : ¬r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
case intro.intro.intro.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
by_cases r j i
no goals
case intro.intro.intro.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
hj : i ∈ support x
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single i (↑x i))
exact ha _ hs
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) 0
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
rw [hr j h, single_eq_of_ne hij, single_zero]
no goals
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) 0
exact Lex.acc_zero hbot
no goals
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (Dfinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (Dfinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : ¬r j i
⊢ Acc (Dfinsupp.Lex r fun i a => s i a) (single j (↑x j))
exact ih _ ⟨h, hij.symm⟩ _