lemma is_local_structomorph_on_cont_diff_groupoid_iff_aux {f : local_homeomorph M M'}
  (hf : lift_prop_on (cont_diff_groupoid ⊤ I).is_local_structomorph_within_at f f.source) :
  smooth_on I I f f.source :=
sorry -- you already proved this

/-- Let `M` and `M'` be smooth manifolds with the same model-with-corners, `I`.  Then `f : M → M'`
is a local structomorphism for `I`, if and only if it is manifold-smooth on the domain of definition
in both directions. -/
lemma is_local_structomorph_on_cont_diff_groupoid_iff (f : local_homeomorph M M') :
  lift_prop_on (cont_diff_groupoid ⊤ I).is_local_structomorph_within_at f f.source
  ↔ smooth_on I I f f.source ∧ smooth_on I I f.symm f.target :=
begin
  split,
  { intros h,
    refine ⟨is_local_structomorph_on_cont_diff_groupoid_iff_aux h, 
      is_local_structomorph_on_cont_diff_groupoid_iff_aux _⟩,
    intros X hX,
    let x := f.symm X,
    have hx : x ∈ f.source := f.symm.maps_to hX,
    let c := chart_at H x,
    let c' := chart_at H X,
    obtain ⟨-, hxf⟩ := h x hx,
    refine ⟨(f.symm.continuous_at hX).continuous_within_at, λ h2x, _⟩,
    obtain ⟨e, he, he', hex⟩ : ∃ e : local_homeomorph H H, e ∈ cont_diff_groupoid ⊤ I ∧
      eq_on (c' ∘ f ∘ c.symm) e (c.symm ⁻¹' f.source ∩ e.source) ∧ c x ∈ e.source,
    { have : c' = chart_at H (f x) := by simp only [f.right_inv hX],
      rw this,
      exact hxf (by simp only [hx] with mfld_simps) },
    have hX' : c' X = e (c (f.symm X)),
    { rw ← he',
      { dsimp only [function.comp],
        have hfX : f.symm X ∈ c.source := by simp only [hX] with mfld_simps,
        rw [c.left_inv hfX, f.right_inv hX] },
      simp only [hX, hex] with mfld_simps, exact hx },    
    refine ⟨e.symm, structure_groupoid.symm _ he, _, _⟩, -- maybe e.symm needs to be restricted further
    { sorry }, -- roughly H₂ in your proof
    rw [hX'], exact e.maps_to hex, },
 [...]