-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n_1 : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ∀ (h : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x),
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
      (iteratedFDerivWithin 𝕜 n f s)
h : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s x
t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x
t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y
a : E
h₁a :
  (𝓝[s] a).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
    (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
      (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
    (iteratedFDerivWithin 𝕜 n f s)
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a
h₄a : a ∈ s
m : (i : Fin (n + 1)) → E
inl :
  ∀ (h : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s x) (t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x)
    (t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y) (a : E)
    (h₁a :
      (𝓝[s] a).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
        (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
          (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
        (iteratedFDerivWithin 𝕜 n f s))
    (h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a) (h₄a : a ∈ s) (m : (i : Fin (n + 1)) → E) ⦃a : E⦄
    (hn : ¬ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x), a ∈ s → a ∈ s
⊢ s ⊆ s
have inr : ∀ (h : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s x) (t₀ : ContDiffWithinAt 𝕜' (↑n : WithTop ℕ∞) f s x)
  (t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s y) (a : E)
  (h₁a :
    (𝓝[s] a).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
      (iteratedFDerivWithin 𝕜 n f s))
  (h₃a : ContDiffWithinAt 𝕜' (↑(n + 1) : WithTop ℕ∞) f s a) (h₄a : a ∈ s) (m : (i : Fin (n + 1)) → E) ⦃a : E⦄
  (hn :
    (𝓝[s] x).EventuallyEq (β := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ E) F)
      (Function.comp (β := ContinuousMultilinearMap.{u_2, 0, u_3, u_4} 𝕜' (fun (i : Fin n) ↦ E) F)
        (restrictScalars 𝕜 (M₁ := fun (i : Fin n) ↦ E)) (iteratedFDerivWithin 𝕜' n f s))
      (iteratedFDerivWithin 𝕜 n f s)),
  a ∈ s → a ∈ s
Tactic: tauto
Cleared hypotheses: hn, h, t₀, t₁, a, h₁a, h₃a, h₄a, m