torsion_exists_subgroup_subset_card_le

lemma torsion_exists_subgroup_subset_card_le {G : Type*} {m : ℕ} (hm : m ≥ 2)    [AddCommGroup G] [Finite G] (htorsion : ∀ x:G, m • x = 0)    {k : ℕ} (H : AddSubgroup G) (hk : k ≤ (H : Set G).ncard) (h'k : k ≠ 0) :    ∃ (K : AddSubgroup G), (K : Set G).ncard ≤ k ∧ k < m * (K : Set G).ncard ∧ K ≤ H := by    let S := {K: AddSubgroup G | K ≤ H ∧ (K : Set G).ncard ≤ k }    have hnon : S.Nonempty := ⟨⊥, by simp [S]; omega⟩    obtain ⟨K, hK, hK'⟩ := S.toFinite.exists_maximalFor      (fun K : AddSubgroup G ↦ (K : Set G).ncard) S hnon    refine ⟨K, hK.2, ?_, hK.1⟩    rcases LE.le.lt_or_eq hK.1 with heq | heq    · have hneq : (K:Set G) ≠ (H:Set G) := by        contrapose! heq        simp only [SetLike.coe_set_eq] at heq        simp only [heq, lt_self_iff_false, not_false_eq_true]      obtain ⟨a, ha, ha'⟩ := exists_of_ssubset (ssubset_of_subset_of_ne hK.1 hneq)      let Z := AddSubgroup.zmultiples a      let H' := K ⊔ Z      contrapose! ha'      have hcard : (H' : Set G).ncard ≤ k := by        apply le_trans _ ha'        rw [AddSubgroup.normal_add K Z, Nat.mul_comm]        calc          _ ≤ (K : Set G).ncard * Nat.card (Z : Set G) := Set.natCard_add_le          _ ≤ _ := by            gcongr            rw [SetLike.coe_sort_coe, Nat.card_zmultiples a]            apply addOrderOf_le_of_nsmul_eq_zero (Nat.zero_lt_of_lt hm) (htorsion a)      have hH' : H' ≤ H := by        simpa only [sup_le_iff, hK.1, AddSubgroup.zmultiples_le, true_and, H', Z]      have hsub : (K:Set G) ⊆ (H':Set G) := SetLike.coe_subset_coe.mpr le_sup_left      have hcard' : (K : Set G).ncard ≤ (H' : Set G).ncard := by gcongr; exact Set.toFinite _      have : (K:Set G) = (H':Set G) := by          apply (Set.subset_iff_eq_of_ncard_le ?_ ?_).mp hsub          · rw [← Nat.card_coe_set_eq (H':Set G), ← Nat.card_coe_set_eq (K:Set G)]            exact hK' ⟨hH', hcard⟩ hcard'          exact Set.toFinite (H':Set G)      rw [this]      exact (le_sup_right : AddSubgroup.zmultiples a ≤ H') (AddSubgroup.mem_zmultiples a)    rw [heq]    exact lt_of_le_of_lt hk ((Nat.lt_mul_iff_one_lt_left Nat.card_pos).mpr hm)