ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : support x = t
⊢ (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), i ∈ support x → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
generalize ht : x.support = t
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : support x = t
⊢ (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
revert x
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = ∅ → (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x

case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = insert b t →
      (∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
induction' t using Finset.induction with b t hb ih
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
⊢ Acc (Dfinsupp.Lex r s) (erase b x)
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = insert b t →
      (∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
refine' fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) _
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (Dfinsupp.Lex r s) (single a (↑(erase b x) a))
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
⊢ Acc (Dfinsupp.Lex r s) (erase b x)
refine' ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => _
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (Dfinsupp.Lex r s) (single a (↑x a))
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (Dfinsupp.Lex r s) (single a (↑(erase b x) a))
rw [erase_ne (ha.ne_of_not_mem hb)]
no goals
case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (Dfinsupp.Lex r s) (single a (↑x a))
exact h a (Finset.mem_insert_of_mem ha)
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = ∅ → (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
intro x ht
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑0 i))) → Acc (Dfinsupp.Lex r s) 0
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
rw [support_eq_empty.1 ht]
no goals
case empty
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (Dfinsupp.Lex r s) (single i (↑0 i))) → Acc (Dfinsupp.Lex r s) 0
exact fun _ => Lex.acc_zero hbot
no goals
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (Dfinsupp.Lex r s) (single i (↑x i))) → Acc (Dfinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (Dfinsupp.Lex r s) (single i (↑x i))
⊢ support (erase b x) = t
rw [support_erase, ht, Finset.erase_insert hb]