wlog_notInCoset

lemma wlog_notInCoset (hA : A.Nonempty) (hB : B.Nonempty) :    ∃ (G' : AddSubgroup G) (A' B' : Set (G' : Set G)),    IsShift A A' ∧ IsShift B B' ∧ NotInCoset A' B' := by  obtain ⟨x, hx⟩ := hA  obtain ⟨y, hy⟩ := hB  set G' := AddSubgroup.closure ((A - A) ∪ (B - B)) with hG'  set A' : Set (G' : Set G) := (↑) ⁻¹' ((-x) +ᵥ A) with hA'  set B' : Set (G' : Set G) := (↑) ⁻¹' ((-y) +ᵥ B) with hB'  have hxA : -x +ᵥ A ⊆ range ((↑) : G' → G) := by    simp only [← singleton_add', ← neg_singleton, neg_add_eq_sub, Subtype.range_coe_subtype]    exact (sub_subset_sub_left <| singleton_subset_iff.2 hx).trans <| (subset_union_left ..).trans      AddSubgroup.subset_closure  have hyB : -y +ᵥ B ⊆ range ((↑) : G' → G) := by    simp only [← singleton_add', ← neg_singleton, neg_add_eq_sub, Subtype.range_coe_subtype]    exact (sub_subset_sub_left <| singleton_subset_iff.2 hy).trans <| (subset_union_right ..).trans      AddSubgroup.subset_closure  have hA : IsShift A A' := ⟨x, by rwa [hA', Set.image_preimage_eq_of_subset, vadd_neg_vadd]⟩  have hB : IsShift B B' := ⟨y, by rwa [hB', Set.image_preimage_eq_of_subset, vadd_neg_vadd]⟩  refine ⟨G', A', B', hA, hB, ?_⟩  unfold NotInCoset  convert! AddSubgroup.closure_preimage_eq_top ((A - A) ∪ (B - B))  simp_rw [preimage_union, hA.sub_self_congr, hB.sub_self_congr]  rw [preimage_sub, preimage_sub]  · simp only [A', B', Subtype.image_preimage_coe]    simp only [SetLike.coe_sort_coe, AddSubgroup.coe_subtype, preimage_inter]    rw [Subtype.coe_preimage_self, Subtype.coe_preimage_self, Subtype.coe_preimage_self,      Subtype.coe_preimage_self]    simp only [univ_inter]    rfl  all_goals apply_rules [Subtype.coe_injective, (image_preimage_subset ..).trans, hxA, hyB]