awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (hypothesis)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ),
    HSMul.hSMul (β := 𝕜) n.factorial ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜) =
      (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
          (a : (i : Fin n) → 𝕜) → 𝕜)
        fun (x : Fin n) ↦ 1 :
      𝕜)
    ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)
have h_fact_smul₁ : ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
Tactic: simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const, Finset.card_univ,
    Fintype.card_fin, smul_eq_mul, nsmul_eq_mul, one_pow, one_mul] at h_fact_smul
Cleared hypotheses: h_fact_smul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) n :
          (a : (i : Fin n) → 𝕜) → 𝕜)
        fun (x : Fin n) ↦ 1 :
      𝕜)
    ((p n : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1 : 𝕜)
have h : iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n ∨ Eq.{u_3 + 1} (α := 𝕜) (∏ x : Fin n, 1) 0
Tactic: simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff,
    FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul, mul_eq_mul_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n ∨ Eq.{u_3 + 1} (α := 𝕜) (∏ x : Fin n, 1) 0
have h : iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ iteratedDeriv n f x / (↑n.factorial : 𝕜) = p.coeff n
have h : Ne.{u_3 + 1} (α := 𝕜) (↑n.factorial : 𝕜) 0
Tactic: rw [div_eq_iff, mul_comm, h_fact_smul, ← iteratedDeriv_eq_iteratedFDeriv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul :
  ∀ (n : ℕ), (↑n.factorial : 𝕜) * p.coeff n = (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → 𝕜) → 𝕜) fun (x : Fin n) ↦ 1
⊢ Ne.{u_3 + 1} (α := 𝕜) (↑n.factorial : 𝕜) 0
have h : ¬n.factorial = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
x : 𝕜
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0
have zero : ∀ {c : F}, iteratedDeriv 0 (fun (x : 𝕜) ↦ c) x = if Eq (α := ℕ) 0 0 then c else 0
Tactic: induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDeriv_succ', h]
Cleared hypotheses: n, c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
x : 𝕜
zero : ∀ {c : F}, iteratedDeriv 0 (fun (x : 𝕜) ↦ c) x = if Eq (α := ℕ) 0 0 then c else 0
⊢ iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0
have succ : ∀ (n : ℕ) (h : ∀ {c : F}, iteratedDeriv n (fun (x : 𝕜) ↦ c) x = if n = 0 then c else 0) {c : F},
  iteratedDeriv (n + 1) (fun (x : 𝕜) ↦ c) x = if n + 1 = 0 then c else 0
Tactic: induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDeriv_succ', h]
Cleared hypotheses: n, c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0
have zero : ∀ {c : F}, iteratedDerivWithin 0 (fun (x : 𝕜) ↦ c) s x = if Eq (α := ℕ) 0 0 then c else 0
Tactic: induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDerivWithin_succ', Pi.zero_def, h]
Cleared hypotheses: n, c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
c : F
s : Set 𝕜
x : 𝕜
zero : ∀ {c : F}, iteratedDerivWithin 0 (fun (x : 𝕜) ↦ c) s x = if Eq (α := ℕ) 0 0 then c else 0
⊢ iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0
have succ : ∀ (n : ℕ) (h : ∀ {c : F}, iteratedDerivWithin n (fun (x : 𝕜) ↦ c) s x = if n = 0 then c else 0) {c : F},
  iteratedDerivWithin (n + 1) (fun (x : 𝕜) ↦ c) s x = if n + 1 = 0 then c else 0
Tactic: induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDerivWithin_succ', Pi.zero_def, h]
Cleared hypotheses: n, c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
⊢ ContDiff 𝕜 (↑(n + 1) : ℕ∞ω) f ↔ ContDiff 𝕜 (↑n : ℕ∞ω) f ∧ ContDiff 𝕜 1 (iteratedDeriv n f)
have simp : ((∀ m ≤ n + 1,
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (iteratedDeriv m f)) ∧
    ∀ m < n + 1, Differentiable 𝕜 (iteratedDeriv m f)) ↔
  ((∀ m ≤ n,
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
            PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (iteratedDeriv m f)) ∧
      ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)) ∧
    Differentiable 𝕜 (iteratedDeriv n f) ∧
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (iteratedDeriv (n + 1) f)
Tactic: simp only [contDiff_nat_iff_iteratedDeriv, contDiff_one_iff_deriv, ← iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x
have simp : Eq.{u_3 + 1} (α := F)
  ((FormalMultilinearSeries.taylorComp (ftaylorSeriesWithin 𝕜 g t (f x)) (ftaylorSeriesWithin 𝕜 f s x) i :
        (a : (i : Fin i) → 𝕜) → F)
      fun (x : Fin i) ↦ 1 :
    F)
  (∑ x_1 : OrderedFinpartition i,
      (iteratedFDerivWithin 𝕜 x_1.length g t (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
        (iteratedFDerivWithin 𝕜 (x_1.partSize j) f s x : (a : (i : Fin (x_1.partSize j)) → 𝕜) → E)
          fun (x : Fin (x_1.partSize j)) ↦ 1 :
    F)
Tactic: simp only [iteratedDerivWithin, iteratedFDerivWithin_comp hg hf ht hs hx hst hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : (↑i : ℕ∞ω) ≤ n
⊢ iteratedDeriv i (g ∘ f) x =
    ∑ c : OrderedFinpartition i,
      (iteratedFDeriv 𝕜 c.length g (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDeriv (c.partSize j) f x
have simp : iteratedDerivWithin i (g ∘ f) univ x =
  ∑ x_1 : OrderedFinpartition i,
    (iteratedFDerivWithin 𝕜 x_1.length g univ (f x) : (a : (i : Fin x_1.length) → E) → F) fun (j : Fin x_1.length) ↦
      iteratedDerivWithin (x_1.partSize j) f univ x
Tactic: simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ iteratedDerivWithin 2 (g ∘ f) s x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)
have rw : (∑ c : OrderedFinpartition 2,
    (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
      iteratedDerivWithin (c.partSize j) f s x) =
  HAdd.hAdd (α := F) (β := F)
    ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
    ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)
Tactic: rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDeriv 𝕜 2 g (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ deriv f x : F)
      ((fderiv 𝕜 g (f x) : (a : E) → F) (iteratedDeriv 2 f x) : F)
have simp : iteratedDerivWithin 2 (g ∘ f) univ x =
  HAdd.hAdd (α := F) (β := F)
    ((iteratedFDerivWithin 𝕜 2 g univ (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f univ x : F)
    ((fderivWithin 𝕜 g univ (f x) : (a : E) → F) (iteratedDerivWithin 2 f univ x) : F)
Tactic: simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ,
    ← derivWithin_univ, ← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ iteratedDerivWithin 3 (g ∘ f) s x =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F))
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)
have rw : (∑ c : OrderedFinpartition 3,
    (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
      iteratedDerivWithin (c.partSize j) f s x) =
  HAdd.hAdd (β := F)
    (HAdd.hAdd (α := F) (β := F)
        ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          F) +
      HSMul.hSMul (α := ℕ) (β := F) 2
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
          F))
    ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)
Tactic: rw [iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf ht hs hx hst le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
j : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ Eq (α := ℕ) (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ)
    1
have 0 : Eq (α := ℕ)
  (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩) :
    ℕ)
  (1 : ℕ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
j : Fin (HAdd.hAdd (α := ℕ) 2 1)
0 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    (1 : ℕ)
⊢ Eq (α := ℕ) (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ)
    1
have 1 : Eq (α := ℕ)
  (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩) :
    ℕ)
  (1 : ℕ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
j : Fin (HAdd.hAdd (α := ℕ) 2 1)
0 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) :
      ℕ)
    (1 : ℕ)
1 :
  Eq (α := ℕ)
    (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) :
      ℕ)
    (1 : ℕ)
⊢ Eq (α := ℕ) (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ)
    1
have 2 : Eq (α := ℕ)
  (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩) :
    ℕ)
  (1 : ℕ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (j : Fin 3) ↦
          iteratedDerivWithin
            (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j) f s
            x :
        F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
            iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
              iteratedDerivWithin
                (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j) f
                s x :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
                iteratedDerivWithin
                  (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j)
                  f s x :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)))) =
    HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
                ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F))))
have this : ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
  Eq (α := ℕ) (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ)
    1
Tactic: have (j : _) : (Fin.cons 1 (Fin.cons 1 fun _ ↦ 1) : Fin 3 → ℕ) j = 1 := by
    fin_cases j <;> rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
this :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
⊢ HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (j : Fin 3) ↦
          iteratedDerivWithin
            (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j) f s
            x :
        F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
            iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
              iteratedDerivWithin
                (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j) f
                s x :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
                iteratedDerivWithin
                  (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j)
                  f s x :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)))) =
    HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
                ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F))))
have e_a : Eq.{u_2 + 1} (α := (i : Fin 3) → E)
  (fun (j : Fin 3) ↦
    iteratedDerivWithin
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j) f s x)
  fun (x_1 : Fin 3) ↦ derivWithin f s x
Tactic: congr