awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - i) g s x)
have hB : ‖B‖ ≤ 1
Tactic: have hB : ‖B‖ ≤ 1 := by
    simp only [B, ContinuousLinearMap.opNorm_flip, ContinuousLinearMap.apply]
    refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun f => ?_
    simp only [ContinuousLinearMap.coe_id', id, one_mul]
    rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : ℕ∞ω
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDeriv 𝕜 i f x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv 𝕜 (n - i) g x)
have simp : norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
    (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) univ x) ≤
  ∑ x_1 ∈ Finset.range (n + 1),
    (↑(n.choose x_1) : ℝ) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) (F →L[𝕜] G))
          (iteratedFDerivWithin 𝕜 x_1 f univ x) *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) F)
        (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
have h : norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
    (L.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E) (iteratedFDerivWithin 𝕜 n f s x)) ≤
  ‖L‖ * norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
Tactic: have h := L.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
h :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (L.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E) (iteratedFDerivWithin 𝕜 n f s x)) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
have rwa : ∀
  (h :
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
        (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
      ‖L‖ *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
          (iteratedFDerivWithin 𝕜 n f s x)),
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
Tactic: rwa [← L.iteratedFDerivWithin_comp_left hf hs hx hn] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv 𝕜 n ((⇑L : (a : F) → G) ∘ f) x) ≤
    ‖L‖ * norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f x)
have simp : norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
    (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) univ x) ≤
  ‖L‖ *
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: simp only [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) c) s x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)
have apply : norm (E := (F →L[𝕜] G) →L[𝕜] G)
      ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) *
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x) ≤
  ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)
Tactic: apply ((ContinuousLinearMap.apply 𝕜 G c).norm_iteratedFDerivWithin_comp_left hf hs hx hn).trans
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] G)
        ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)
have hbc : norm (E := (F →L[𝕜] G) →L[𝕜] G)
    ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) ≤
  ‖c‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] G)
      ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) ≤
    ‖c‖
have hbc : ∀ (f : F →L[𝕜] G),
  norm.{uG} (E := G)
      ((((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) : (a : F →L[𝕜] G) → G)
          f :
        G) ≤
    ‖c‖ * ‖f‖
Tactic: refine (ContinuousLinearMap.apply 𝕜 G c).opNorm_le_bound (norm_nonneg _) fun f => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f_1 : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f_1 s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
f : F →L[𝕜] G
⊢ norm.{uG} (E := G)
      ((((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) : (a : F →L[𝕜] G) → G)
          f :
        G) ≤
    ‖c‖ * ‖f‖
have hbc : norm.{uG} (E := G) ((f : (a : F) → G) c : G) ≤ ‖f‖ * ‖c‖
Tactic: rw [ContinuousLinearMap.apply_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.CPolynomial (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f s
have suffices : ContDiffOn 𝕜 n f t
Tactic: suffices ContDiffOn 𝕜 n f t from this.mono h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.CPolynomial (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
⊢ ContDiffOn 𝕜 n f t
have t_open : IsOpen t
Tactic: have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.CPolynomial (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
⊢ ContDiffOn 𝕜 n f t
have suffices : AnalyticOnNhd 𝕜 f t
Tactic: suffices AnalyticOnNhd 𝕜 f t by
    have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
    exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.CPolynomial (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
⊢ AnalyticOnNhd 𝕜 f t
have H : CPolynomialOn 𝕜 f t
Tactic: have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hg : ContDiffWithinAt 𝕜 ω g t (f x)
hf h'f : ContDiffWithinAt 𝕜 ω f s x
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have obtain : ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (hp : HasFTaylorSeriesUpToOn ω f p u)
  (h'p :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i)
        u),
  ContDiffWithinAt 𝕜 ω (g ∘ f) s x
Tactic: obtain ⟨u, hu, p, hp, h'p⟩ := h'f
Cleared hypotheses: h'f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hg : ContDiffWithinAt 𝕜 ω g t (f x)
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have obtain : ∀ (v : Set F) (hv : v ∈ 𝓝[insert (f x) t] f x) (q : F → FormalMultilinearSeries 𝕜 F G)
  (hq : HasFTaylorSeriesUpToOn ω g q v)
  (h'q :
    ∀ (i : ℕ),
      AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i)
        v),
  ContDiffWithinAt 𝕜 ω (g ∘ f) s x
Tactic: obtain ⟨v, hv, q, hq, h'q⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have wv : w ⊆ f ⁻¹' v
Tactic: have wv : w ⊆ f ⁻¹' v := fun y hy => hy.2.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have wu : w ⊆ u
Tactic: have wu : w ⊆ u := fun y hy => hy.2.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have refine_1 : w ∈ 𝓝[insert x s] x
Tactic: refine ⟨w, ?_, fun y ↦ (q (f y)).taylorComp (p y), hq.comp (hp.mono wu) wv, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
refine_1 : w ∈ 𝓝[insert x s] x
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
have refine_2 : ∀ (i : ℕ),
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (fun (x : E) ↦ (fun (y : E) ↦ (q (f y)).taylorComp (p y)) x i) w
Tactic: refine ⟨w, ?_, fun y ↦ (q (f y)).taylorComp (p y), hq.comp (hp.mono wu) wv, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ w ∈ 𝓝[insert x s] x
have apply : f ⁻¹' v ∈ 𝓝[insert x s] x
Tactic: apply inter_mem self_mem_nhdsWithin (inter_mem hu ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ f ⁻¹' v ∈ 𝓝[insert x s] x
have apply : v ∈ 𝓝[f '' insert x s] f x
Tactic: apply (continuousWithinAt_insert_self.2 hf.continuousWithinAt).preimage_mem_nhdsWithin'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ v ∈ 𝓝[f '' insert x s] f x
have apply : f '' insert x s ⊆ insert (f x) t
Tactic: apply nhdsWithin_mono _ _ hv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Comp (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin i) ↦ F) G) (fun (x : F) ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ f '' insert x s ⊆ insert (f x) t
have simp : insert (f x) (f '' s) ⊆ insert (f x) t
Tactic: simp only [image_insert_eq]