exists_card_inter_add_eq_sSup

lemma exists_card_inter_add_eq_sSup (H : AddSubgroup G) {A : Set G} (hA : A.Nonempty) :    ∃ t : G, (Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G)        = sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G})      ∧ 0 < Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) := by  set k := sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G}  rcases exists_mem_card_inter_add H hA with ⟨n, n_pos, hn⟩  have : k ∈ {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} :=    Nat.sSup_mem ⟨n, hn⟩ bddAbove_card_inter_add  rcases this with ⟨t, ht⟩  have : 0 < Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) := by    apply lt_of_lt_of_le n_pos    rw [ht]    exact le_csSup bddAbove_card_inter_add hn  exact ⟨t, ht, this⟩