-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ∞
hf : ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
zero : ∀ (hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)), ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f.symm : F → E) a
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
        ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a)
    (hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
top :
  ∀
    (Itop :
      ∀ (n : ℕ) (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
        ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a)
    (hf : ContDiffAt 𝕜 ∞ (↑f : E → F) ((↑f.symm : F → E) a)), ContDiffAt 𝕜 ∞ (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
induction n using ENat.nat_induction with
    | zero =>
      apply contDiffAt_zero.2
      exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
    | succ n IH =>
      obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
      apply contDiffAt_succ_iff_hasFDerivAt.2
      -- For showing `n.succ` times continuous differentiability (the main inductive step), it
      -- suffices to produce the derivative and show that it is `n` times continuously
      -- differentiable
      have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
      -- This follows by a bootstrapping formula expressing the derivative as a
      -- function of `f` itself
      refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
      · -- We first check that the derivative of `f` is that formula
        have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
          have hf₀' := f₀'.nhds
          rw [← eq_f₀'] at hf₀'
          exact hf'.continuousAt.preimage_mem_nhds hf₀'
        obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
        use f.target ∩ f.symm ⁻¹' t
        refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
        · exact f.isOpen_inter_preimage_symm ht
        · exact mem_inter ha (mem_preimage.mpr htf)
        intro x hx
        obtain ⟨hxu, e, he⟩ := htu hx.2
        have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu
        convert! f.hasFDerivAt_symm hx.1 h_deriv
        simp [← he]
      · -- Then we check that the formula, being a composition of `ContDiff` pieces, is
        -- itself `ContDiff`
        have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
          rw [eq_f₀']
          exact contDiffAt_map_inverse _
        have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
          refine IH (hf.of_le ?_)
          norm_cast
          exact Nat.le_succ n
        exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
    | top Itop => exact contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)

Premises used: Iff.mpr, Fin.succ, PartialEquiv.target, ContinuousLinearMap.zero, contDiffAt_succ_iff_hasFDerivAt, Iff.mp, contDiffAt_zero, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm