mf_injOn

lemma mf_injOn : InjOn (mf k n j) {u | x ∈ 𝓘 u.1} := fun u mu u' mu' e ↦ by  set m := mf k n j u  have iu : smul 100 u.1 ≤ smul 1 m.1 := (exists_smul_le_of_𝔘₃ u).choose_spec  have iu' : smul 100 u'.1 ≤ smul 1 m.1 := e ▸ (exists_smul_le_of_𝔘₃ u').choose_spec  have su : ball_{𝓘 m.1} (𝒬 m.1) 1 ⊆ ball_{𝓘 u.1} (𝒬 u.1) 100 := iu.2  have su' : ball_{𝓘 m.1} (𝒬 m.1) 1 ⊆ ball_{𝓘 u'.1} (𝒬 u'.1) 100 := iu'.2  have nd : ¬Disjoint (ball_{𝓘 u.1} (𝒬 u.1) 100) (ball_{𝓘 u'.1} (𝒬 u'.1) 100) := by    rw [not_disjoint_iff]    use 𝒬 m.1, su (mem_ball_self zero_lt_one), su' (mem_ball_self zero_lt_one)  by_contra! h; rw [← Subtype.coe_ne_coe] at h; apply absurd _ nd  have nr : ¬URel k n j u.1 u'.1 := by contrapose! h; exact EquivalenceOn.reprs_inj u.2 u'.2 h  have n𝓘 : 𝓘 u.1 ≠ 𝓘 u'.1 := by    contrapose! nr; rw [disjoint_comm] at nd    exact urel_of_not_disjoint (𝔘₃_subset_𝔘₂ u.2) nr.symm nd  rcases le_or_gt (s (𝓘 u.1)) (s (𝓘 u'.1)) with hs | hs  · have hu := lt_of_le_of_ne ((le_or_disjoint hs).resolve_right      (not_disjoint_iff.mpr ⟨_, mu, mu'⟩)) n𝓘    have u₁ := (𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁) u.2    exact u₁.2 u' ((𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁ |>.trans 𝔘₁_subset_ℭ₁) u'.2) hu  · have hu := lt_of_le_of_ne ((le_or_disjoint hs.le).resolve_right      (not_disjoint_iff.mpr ⟨_, mu', mu⟩)) n𝓘.symm    have u'₁ := (𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁) u'.2    exact (u'₁.2 u ((𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁ |>.trans 𝔘₁_subset_ℭ₁) u.2) hu).symm