no goals
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (Dfinsupp.Lex r s) (single i (↑x i))
hu : Acc (Dfinsupp.Lex r s) (erase i x)
⊢ Acc (Dfinsupp.Lex r s) x
classical
  convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{i}, _⟩
    (InvImage.accessible snd <| hs.prod_gameAdd hu)
  convert piecewise_single_erase x i
case h.e'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (Dfinsupp.Lex r s) (single i (↑x i))
hu : Acc (Dfinsupp.Lex r s) (erase i x)
⊢ piecewise ({i}, single i (↑x i), erase i x).snd.fst ({i}, single i (↑x i), erase i x).snd.snd
      ({i}, single i (↑x i), erase i x).fst =
    x
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (Dfinsupp.Lex r s) (single i (↑x i))
hu : Acc (Dfinsupp.Lex r s) (erase i x)
⊢ Acc (Dfinsupp.Lex r s) x
convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{i}, _⟩
  (InvImage.accessible snd <| hs.prod_gameAdd hu)
no goals
case h.e'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (Dfinsupp.Lex r s) (single i (↑x i))
hu : Acc (Dfinsupp.Lex r s) (erase i x)
⊢ piecewise ({i}, single i (↑x i), erase i x).snd.fst ({i}, single i (↑x i), erase i x).snd.snd
      ({i}, single i (↑x i), erase i x).fst =
    x
convert piecewise_single_erase x i