∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G}
  {g : ι → G} {s : Finset ι} (j : ι) (y : G)
  (motive : (∃ i, ∃ (_ : i ∈ {a ∈ s | ¬H a = H j}), y ∈ g i +ᵥ ↑(H i)) → Prop)
  (x : ∃ i, ∃ (_ : i ∈ {a ∈ s | ¬H a = H j}), y ∈ g i +ᵥ ↑(H i)),
  (∀ (i : ι) (hi : i ∈ {a ∈ s | ¬H a = H j}) (hy : y ∈ g i +ᵥ ↑(H i)), motive ⋯) → motive x