[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ LinearMap.range (ContinuousLinearMap.prod f' φ') ≠ ⊤
[PROOFSTEP]
intro htop
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
⊢ False
[PROOFSTEP]
set fφ := fun x => (f x, φ x)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
fφ : E → F × ℝ := fun x => (f x, φ x)
⊢ False
[PROOFSTEP]
have A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀) :=
  by
  change map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
  rw [← map_map, nhdsWithin, map_inf_principal_preimage, (hf'.prod hφ').map_nhds_eq_of_surj htop]
  exact map_snd_nhdsWithin _
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
fφ : E → F × ℝ := fun x => (f x, φ x)
⊢ map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)
[PROOFSTEP]
change map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
fφ : E → F × ℝ := fun x => (f x, φ x)
⊢ map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.fst = f x₀}] x₀) = 𝓝 (φ x₀)
[PROOFSTEP]
rw [← map_map, nhdsWithin, map_inf_principal_preimage, (hf'.prod hφ').map_nhds_eq_of_surj htop]
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
fφ : E → F × ℝ := fun x => (f x, φ x)
⊢ map Prod.snd (𝓝 (f x₀, φ x₀) ⊓ 𝓟 {p | p.fst = f x₀}) = 𝓝 (φ x₀)
[PROOFSTEP]
exact map_snd_nhdsWithin _
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : LinearMap.range (ContinuousLinearMap.prod f' φ') = ⊤
fφ : E → F × ℝ := fun x => (f x, φ x)
A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)
⊢ False
[PROOFSTEP]
exact hextr.not_nhds_le_map A.ge
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
[PROOFSTEP]
rcases Submodule.exists_le_ker_of_lt_top _ (lt_top_iff_ne_top.2 <| hextr.range_ne_top_of_hasStrictFDerivAt hf' hφ') with
  ⟨Λ', h0, hΛ'⟩
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ' : F × ℝ →ₗ[ℝ] ℝ
h0 : Λ' ≠ 0
hΛ' : LinearMap.range (ContinuousLinearMap.prod f' φ') ≤ LinearMap.ker Λ'
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
[PROOFSTEP]
set e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  ((LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm).trans (LinearMap.coprodEquiv ℝ)
[GOAL]
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ' : F × ℝ →ₗ[ℝ] ℝ
h0 : Λ' ≠ 0
hΛ' : LinearMap.range (ContinuousLinearMap.prod f' φ') ≤ LinearMap.ker Λ'
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.trans
    (LinearEquiv.prod (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)))
    (LinearMap.coprodEquiv ℝ)
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
[PROOFSTEP]
rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩
[GOAL]
case intro.intro.intro.mk
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.trans
    (LinearEquiv.prod (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)))
    (LinearMap.coprodEquiv ℝ)
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : ↑e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (ContinuousLinearMap.prod f' φ') ≤ LinearMap.ker (↑e (Λ, Λ₀))
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
[PROOFSTEP]
refine' ⟨Λ, Λ₀, e.map_ne_zero_iff.1 h0, fun x => _⟩
[GOAL]
case intro.intro.intro.mk
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.trans
    (LinearEquiv.prod (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)))
    (LinearMap.coprodEquiv ℝ)
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : ↑e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (ContinuousLinearMap.prod f' φ') ≤ LinearMap.ker (↑e (Λ, Λ₀))
x : E
⊢ ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
[PROOFSTEP]
convert LinearMap.congr_fun (LinearMap.range_le_ker_iff.1 hΛ') x using 1
  -- squeezed `simp [mul_comm]` to speed up elaboration
[GOAL]
case h.e'_2
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.trans
    (LinearEquiv.prod (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)))
    (LinearMap.coprodEquiv ℝ)
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : ↑e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (ContinuousLinearMap.prod f' φ') ≤ LinearMap.ker (↑e (Λ, Λ₀))
x : E
⊢ ↑Λ (↑f' x) + Λ₀ • ↑φ' x = ↑(LinearMap.comp (↑e (Λ, Λ₀)) ↑(ContinuousLinearMap.prod f' φ')) x
[PROOFSTEP]
simp only [smul_eq_mul, LinearEquiv.trans_apply, LinearEquiv.prod_apply, LinearEquiv.refl_apply,
  LinearMap.ringLmapEquivSelf_symm_apply, LinearMap.coprodEquiv_apply, ContinuousLinearMap.coe_prod,
  LinearMap.coprod_comp_prod, LinearMap.add_apply, LinearMap.coe_comp, ContinuousLinearMap.coe_coe, Function.comp_apply,
  LinearMap.coe_smulRight, LinearMap.one_apply, mul_comm]
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ ∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
[PROOFSTEP]
obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ'
[GOAL]
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
⊢ ∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
[PROOFSTEP]
refine' ⟨Λ 1, Λ₀, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
⊢ (↑Λ 1, Λ₀) ≠ 0
[PROOFSTEP]
contrapose! hΛ
[GOAL]
case intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
hΛ : (↑Λ 1, Λ₀) = 0
⊢ (Λ, Λ₀) = 0
[PROOFSTEP]
simp only [Prod.mk_eq_zero] at hΛ ⊢
[GOAL]
case intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
hΛ : ↑Λ 1 = 0 ∧ Λ₀ = 0
⊢ Λ = 0 ∧ Λ₀ = 0
[PROOFSTEP]
refine' ⟨LinearMap.ext fun x => _, hΛ.2⟩
[GOAL]
case intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
hΛ : ↑Λ 1 = 0 ∧ Λ₀ = 0
x : ℝ
⊢ ↑Λ x = ↑0 x
[PROOFSTEP]
simpa [hΛ.1] using Λ.map_smul x 1
[GOAL]
case intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
⊢ ↑Λ 1 • f' + Λ₀ • φ' = 0
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
x : E
⊢ ↑(↑Λ 1 • f' + Λ₀ • φ') x = ↑0 x
[PROOFSTEP]
have H₁ : Λ (f' x) = f' x * Λ 1 := by simpa only [mul_one, Algebra.id.smul_eq_mul] using Λ.map_smul (f' x) 1
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
x : E
⊢ ↑Λ (↑f' x) = ↑f' x * ↑Λ 1
[PROOFSTEP]
simpa only [mul_one, Algebra.id.smul_eq_mul] using Λ.map_smul (f' x) 1
[GOAL]
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
x : E
H₁ : ↑Λ (↑f' x) = ↑f' x * ↑Λ 1
⊢ ↑(↑Λ 1 • f' + Λ₀ • φ') x = ↑0 x
[PROOFSTEP]
have H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0 := by simpa only [Algebra.id.smul_eq_mul, H₁] using hfΛ x
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
x : E
H₁ : ↑Λ (↑f' x) = ↑f' x * ↑Λ 1
⊢ ↑f' x * ↑Λ 1 + Λ₀ * ↑φ' x = 0
[PROOFSTEP]
simpa only [Algebra.id.smul_eq_mul, H₁] using hfΛ x
[GOAL]
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
f : E → ℝ
f' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), ↑Λ (↑f' x) + Λ₀ • ↑φ' x = 0
x : E
H₁ : ↑Λ (↑f' x) = ↑f' x * ↑Λ 1
H₂ : ↑f' x * ↑Λ 1 + Λ₀ * ↑φ' x = 0
⊢ ↑(↑Λ 1 • f' + Λ₀ • φ') x = ↑0 x
[PROOFSTEP]
simpa [mul_comm] using H₂
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
[GOAL]
case hextr
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
⊢ IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
[PROOFSTEP]
simpa only [Function.funext_iff] using hextr
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i) hφ' with ⟨Λ, Λ₀, h0, hsum⟩
[GOAL]
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
Λ : Module.Dual ℝ (ι → ℝ)
Λ₀ : ℝ
h0 : (Λ, Λ₀) ≠ 0
hsum : ∀ (x : E), ↑Λ (↑(ContinuousLinearMap.pi fun i => f' i) x) + Λ₀ • ↑φ' x = 0
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
rcases(LinearEquiv.piRing ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 : (↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ, Λ₀) ≠ 0
hsum :
  ∀ (x : E),
    ↑(↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ) (↑(ContinuousLinearMap.pi fun i => f' i) x) + Λ₀ • ↑φ' x = 0
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
refine' ⟨Λ, Λ₀, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 : (↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ, Λ₀) ≠ 0
hsum :
  ∀ (x : E),
    ↑(↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ) (↑(ContinuousLinearMap.pi fun i => f' i) x) + Λ₀ • ↑φ' x = 0
⊢ (Λ, Λ₀) ≠ 0
[PROOFSTEP]
simpa only [Ne.def, Prod.ext_iff, LinearEquiv.map_eq_zero_iff, Prod.fst_zero] using h0
[GOAL]
case intro.intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 : (↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ, Λ₀) ≠ 0
hsum :
  ∀ (x : E),
    ↑(↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ) (↑(ContinuousLinearMap.pi fun i => f' i) x) + Λ₀ • ↑φ' x = 0
⊢ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 : (↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ, Λ₀) ≠ 0
hsum :
  ∀ (x : E),
    ↑(↑(LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ)) Λ) (↑(ContinuousLinearMap.pi fun i => f' i) x) + Λ₀ • ↑φ' x = 0
x : E
⊢ ↑(∑ i : ι, Λ i • f' i + Λ₀ • φ') x = ↑0 x
[PROOFSTEP]
simpa [mul_comm] using hsum x
[GOAL]
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')
[PROOFSTEP]
rw [Fintype.linearIndependent_iff]
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
⊢ ¬∀ (g : Option ι → ℝ), ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 → ∀ (i : Option ι), g i = 0
[PROOFSTEP]
push_neg
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
⊢ ∃ g, ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
rcases hextr.exists_multipliers_of_hasStrictFDerivAt hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ g, ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 ∧ ∃ i, g i ≠ 0
[PROOFSTEP]
refine' ⟨Option.elim' Λ₀ Λ, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∑ i : Option ι, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i = 0
[PROOFSTEP]
simpa [add_comm] using hΛf
[GOAL]
case intro.intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
f✝ : E → F
φ : E → ℝ
x₀ : E
f'✝ : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ i, Option.elim' Λ₀ Λ i ≠ 0
[PROOFSTEP]
simpa only [Function.funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne.def, not_forall] using hΛ


[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0
case this α : Type u_1 b : ℂ hb : b ≠ 0 ⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [zero_cpow hx, Pi.zero_apply]
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => 0 ^ x) x = OfNat.ofNat 0 x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = OfNat.ofNat 0 x
[PROOFSTEP]
rw [zero_cpow hx, Pi.zero_apply]
[GOAL]
case this
α : Type u_1
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
[PROOFSTEP]
exact IsOpen.eventually_mem isOpen_ne hb
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => Complex.exp (Complex.log x * b)
case this α : Type u_1 a b : ℂ ha : a ≠ 0 ⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => x ^ b) x = (fun x => Complex.exp (Complex.log x * b)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = Complex.exp (Complex.log x * b)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hx]
[GOAL]
case this
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
[PROOFSTEP]
exact IsOpen.eventually_mem isOpen_ne ha
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)
[PROOFSTEP]
suffices : ∀ᶠ x : ℂ × ℂ in 𝓝 p, x.1 ≠ 0
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => Complex.exp (Complex.log x.fst * x.snd)
case this α : Type u_1 p : ℂ × ℂ hp_fst : p.fst ≠ 0 ⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [cpow_def_of_ne_zero hx]
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => Complex.exp (Complex.log x.fst * x.snd)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
this : ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
x : ℂ × ℂ
hx : x.fst ≠ 0
⊢ x.fst ^ x.snd = Complex.exp (Complex.log x.fst * x.snd)
[PROOFSTEP]
rw [cpow_def_of_ne_zero hx]
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 p, x.fst ≠ 0
[PROOFSTEP]
refine' IsOpen.eventually_mem _ hp_fst
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen fun x => x.fst = 0 → False
[PROOFSTEP]
change IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsOpen {x | x.fst = 0}ᶜ
[PROOFSTEP]
rw [isOpen_compl_iff]
[GOAL]
case this
α : Type u_1
p : ℂ × ℂ
hp_fst : p.fst ≠ 0
⊢ IsClosed {x | x.fst = 0}
[PROOFSTEP]
exact isClosed_eq continuous_fst continuous_const
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) :=
  by
  ext1 b
  rw [cpow_def_of_ne_zero ha]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
⊢ (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
[PROOFSTEP]
ext1 b
[GOAL]
case h
α : Type u_1
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = Complex.exp (Complex.log a * b)
[PROOFSTEP]
rw [cpow_def_of_ne_zero ha]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
rw [cpow_eq]
[GOAL]
α : Type u_1
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => Complex.exp (Complex.log a * x)
⊢ ContinuousAt (fun x => Complex.exp (Complex.log a * x)) b
[PROOFSTEP]
exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)
[GOAL]
α : Type u_1
a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
[GOAL]
case pos
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b
[PROOFSTEP]
exact continuousAt_const
[GOAL]
case neg
α : Type u_1
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x => a ^ x) b
[PROOFSTEP]
exact continuousAt_const_cpow ha
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
have hp_fst_ne_zero : p.fst ≠ 0 := by
  intro h
  cases' hp_fst with hp_fst hp_fst <;>
    · rw [h] at hp_fst
      simp at hp_fst
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
⊢ p.fst ≠ 0
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
h : p.fst = 0
⊢ False
[PROOFSTEP]
cases' hp_fst with hp_fst hp_fst
[GOAL]
case inl
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0 < p.fst.re
⊢ False
[PROOFSTEP]
rw [h] at hp_fst
[GOAL]
case inl
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0 < 0.re
⊢ False
[PROOFSTEP]
simp at hp_fst
[GOAL]
case inr
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : p.fst.im ≠ 0
⊢ False
[PROOFSTEP]
rw [h] at hp_fst
[GOAL]
case inr
α : Type u_1
p : ℂ × ℂ
h : p.fst = 0
hp_fst : 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp at hp_fst
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
rw [continuousAt_congr (cpow_eq_nhds' hp_fst_ne_zero)]
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.exp (Complex.log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp _
[GOAL]
α : Type u_1
p : ℂ × ℂ
hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0
hp_fst_ne_zero : p.fst ≠ 0
⊢ ContinuousAt (fun x => Complex.log x.fst * x.snd) p
[PROOFSTEP]
exact
  ContinuousAt.mul (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
    continuous_snd.continuousAt
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
cases h with
| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
cases h with
| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]

| inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
[GOAL]
case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
exact (continuousAt_const_cpow h).tendsto.comp hf
[GOAL]
case inr
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]

| inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
case inr
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b))
[PROOFSTEP]
exact (continuousAt_const_cpow' h).tendsto.comp hf
[GOAL]
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
  ext1 x
  rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : a ≠ 0
⊢ rpow a = fun x => (↑a ^ ↑x).re
[PROOFSTEP]
ext1 x
[GOAL]
case h
a b : ℝ
h : a ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
[PROOFSTEP]
rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
rw [this]
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
[PROOFSTEP]
refine' Complex.continuous_re.continuousAt.comp _
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
[PROOFSTEP]
refine' (continuousAt_const_cpow _).comp Complex.continuous_ofReal.continuousAt
[GOAL]
a b : ℝ
h : a ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑a ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
  ext1 x
  rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : b ≠ 0
⊢ rpow a = fun x => (↑a ^ ↑x).re
[PROOFSTEP]
ext1 x
[GOAL]
case h
a b : ℝ
h : b ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
[PROOFSTEP]
rw [rpow_eq_pow, rpow_def]
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
[PROOFSTEP]
rw [this]
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
[PROOFSTEP]
refine' Complex.continuous_re.continuousAt.comp _
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
[PROOFSTEP]
refine' (continuousAt_const_cpow' _).comp Complex.continuous_ofReal.continuousAt
[GOAL]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑b ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
[PROOFSTEP]
suffices : ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd) * cos (x.snd * π)
case this p : ℝ × ℝ hp_fst : p.fst < 0 ⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [rpow_def_of_neg hx]
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ (fun x => x.fst ^ x.snd) x = (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) x
[PROOFSTEP]
dsimp only
[GOAL]
p : ℝ × ℝ
hp_fst : p.fst < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
x : ℝ × ℝ
hx : x.fst < 0
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd) * cos (x.snd * π)
[PROOFSTEP]
rw [rpow_def_of_neg hx]
[GOAL]
case this
p : ℝ × ℝ
hp_fst : p.fst < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.fst < 0
[PROOFSTEP]
exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
[PROOFSTEP]
suffices : ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
⊢ (fun x => x.fst ^ x.snd) =ᶠ[𝓝 p] fun x => exp (log x.fst * x.snd)
case this p : ℝ × ℝ hp_fst : 0 < p.fst ⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
[PROOFSTEP]
exact
  this.mono fun x hx => by
    dsimp only
    rw [rpow_def_of_pos hx]
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
x : ℝ × ℝ
hx : 0 < x.fst
⊢ (fun x => x.fst ^ x.snd) x = (fun x => exp (log x.fst * x.snd)) x
[PROOFSTEP]
dsimp only
[GOAL]
p : ℝ × ℝ
hp_fst : 0 < p.fst
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
x : ℝ × ℝ
hx : 0 < x.fst
⊢ x.fst ^ x.snd = exp (log x.fst * x.snd)
[PROOFSTEP]
rw [rpow_def_of_pos hx]
[GOAL]
case this
p : ℝ × ℝ
hp_fst : 0 < p.fst
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.fst
[PROOFSTEP]
exact IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst
[GOAL]
p : ℝ × ℝ
hp : p.fst ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [ne_iff_lt_or_gt] at hp
[GOAL]
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0 ∨ p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases hp with
| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0 ∨ p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases hp with
| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]

| inl hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
  refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
  · refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
    refine' (continuousAt_log _).comp continuous_fst.continuousAt
    exact hp.ne
  · exact continuous_snd.continuousAt.mul continuousAt_const
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
[GOAL]
case inl
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd) * cos (x.snd * π)) p
[PROOFSTEP]
refine' ContinuousAt.mul _ (continuous_cos.continuousAt.comp _)
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => log x.fst) p
[PROOFSTEP]
refine' (continuousAt_log _).comp continuous_fst.continuousAt
[GOAL]
case inl.refine'_1
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ p.fst ≠ 0
[PROOFSTEP]
exact hp.ne
[GOAL]
case inl.refine'_2
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst < 0
⊢ ContinuousAt (fun x => x.snd * π) p
[PROOFSTEP]
exact continuous_snd.continuousAt.mul continuousAt_const
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]

| inr hp =>
  rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
  refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
  refine' (continuousAt_log _).comp continuous_fst.continuousAt
  exact hp.lt.ne.symm
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => exp (log x.fst * x.snd)) p
[PROOFSTEP]
refine' continuous_exp.continuousAt.comp (ContinuousAt.mul _ continuous_snd.continuousAt)
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ ContinuousAt (fun x => log x.fst) p
[PROOFSTEP]
refine' (continuousAt_log _).comp continuous_fst.continuousAt
[GOAL]
case inr
p : ℝ × ℝ
hp✝ : p.fst ≠ 0
hp : p.fst > 0
⊢ p.fst ≠ 0
[PROOFSTEP]
exact hp.lt.ne.symm
[GOAL]
p : ℝ × ℝ
hp : 0 < p.snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) p
[PROOFSTEP]
cases' p with x y
[GOAL]
case mk
x y : ℝ
hp : 0 < (x, y).snd
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
dsimp only at hp
[GOAL]
case mk
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
obtain hx | rfl := ne_or_eq x 0
[GOAL]
case mk.inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
exact continuousAt_rpow_of_ne (x, y) hx
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
  tendsto_exp_atBot.comp ((tendsto_log_nhdsWithin_zero.comp tendsto_fst).atBot_mul hp tendsto_snd)
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have B : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
  squeeze_zero_norm (fun p => abs_rpow_le_exp_log_mul p.1 p.2) A
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have C : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0) :=
  by
  rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
  exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
[GOAL]
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
[PROOFSTEP]
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
[GOAL]
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).fst ^ (0, a).snd = 0
[PROOFSTEP]
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
[GOAL]
case mk.inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p => exp (log p.fst * p.snd)) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}ᶜ] 0 ×ˢ 𝓝 y) (𝓝 0)
C : Tendsto (fun p => p.fst ^ p.snd) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
simpa only [← sup_prod, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ, nhds_prod_eq, ContinuousAt,
  zero_rpow hp.ne'] using B.sup (C.mono_right (pure_le_nhds _))
[GOAL]
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x => x ^ q) x
[PROOFSTEP]
change ContinuousAt ((fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun y : ℝ => (y, q)) x
[GOAL]
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt ((fun p => p.fst ^ p.snd) ∘ fun y => (y, q)) x
[PROOFSTEP]
apply ContinuousAt.comp
[GOAL]
case hg
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, q)
[PROOFSTEP]
exact continuousAt_rpow (x, q) h
[GOAL]
case hf
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun y => (y, q)) x
[PROOFSTEP]
exact (continuous_id'.prod_mk continuous_const).continuousAt
[GOAL]
α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun a => f a ^ 0) l (𝓝 (x ^ 0))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
[PROOFSTEP]
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
[PROOFSTEP]
rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun e => ‖e.fst ^ e.snd‖) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero (fun _ => norm_nonneg _) (fun _ => abs_cpow_le _ _) _
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re / Real.exp (arg x.fst * x.snd.im)) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
simp only [div_eq_mul_inv, ← Real.exp_neg]
[GOAL]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re * Real.exp (-(arg x.fst * x.snd.im))) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
refine' Tendsto.zero_mul_isBoundedUnder_le _ _
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re) (𝓝 (0, z)) (𝓝 0)
[PROOFSTEP]
convert (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _) _
[GOAL]
case h.e'_5.h.e'_3
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = ‖(0, z).fst‖ ^ (re ∘ Prod.snd) (0, z)
[PROOFSTEP]
simp [hz, Real.zero_rpow hz.ne']
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ‖(0, z).fst‖ ≠ 0 ∨ 0 < (re ∘ Prod.snd) (0, z)
[PROOFSTEP]
simp [hz, Real.zero_rpow hz.ne']
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => Real.exp (-(arg x.fst * x.snd.im)))
[PROOFSTEP]
simp only [Function.comp, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
[PROOFSTEP]
rcases exists_gt |im z| with ⟨C, hC⟩
[GOAL]
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
[PROOFSTEP]
refine' ⟨Real.exp (π * C), eventually_map.2 _⟩
[GOAL]
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun x x_1 => x ≤ x_1) (Real.exp (-(arg a.fst * a.snd.im))) (Real.exp (π * C))
[PROOFSTEP]
refine'
  (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono fun z hz =>
    Real.exp_le_exp.2 <| (neg_le_abs_self _).trans _
[GOAL]
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |arg z.fst * z.snd.im| ≤ π * C
[PROOFSTEP]
rw [_root_.abs_mul]
[GOAL]
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |arg z.fst| * |z.snd.im| ≤ π * C
[PROOFSTEP]
exact mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _) Real.pi_pos.le
[GOAL]
p : ℂ × ℂ
h₁ : 0 ≤ p.fst.re ∨ p.fst.im ≠ 0
h₂ : 0 < p.snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) p
[PROOFSTEP]
cases' p with z w
[GOAL]
case mk
z w : ℂ
h₁ : 0 ≤ (z, w).fst.re ∨ (z, w).fst.im ≠ 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
[PROOFSTEP]
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne.def, Classical.not_not, not_le_zero_iff] at h₁
[GOAL]
case mk
z w : ℂ
h₁ : (0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0) ∨ (z, w).fst = 0
h₂ : 0 < (z, w).snd.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
[PROOFSTEP]
rcases h₁ with (h₁ | (rfl : z = 0))
[GOAL]
case mk.inl
z w : ℂ
h₂ : 0 < (z, w).snd.re
h₁ : 0 < (z, w).fst.re ∨ (z, w).fst.im ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (z, w)
case mk.inr w : ℂ h₂ : 0 < (0, w).snd.re ⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, w)
[PROOFSTEP]
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
refine' (continuousAt_cpow (Or.inl _)).comp this
[GOAL]
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ 0 < (↑(x, y).fst, (x, y).snd).fst.re
[PROOFSTEP]
rwa [ofReal_re]
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ :=
  by
  rw [ofReal_zero]
  apply continuousAt_cpow_zero_of_re_pos
  tauto
[GOAL]
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
[PROOFSTEP]
rw [ofReal_zero]
[GOAL]
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
[PROOFSTEP]
apply continuousAt_cpow_zero_of_re_pos
[GOAL]
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
[GOAL]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
B : ContinuousAt (fun p => (↑p.fst, p.snd)) (0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
[PROOFSTEP]
exact @ContinuousAt.comp (ℝ × ℂ) (ℂ × ℂ) ℂ _ _ _ _ (fun p => ⟨↑p.1, p.2⟩) ⟨0, y⟩ A B
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y)
  by
  refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
  exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
[PROOFSTEP]
refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
[GOAL]
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ∀ (x : ℝ × ℂ),
    x ∈ Set.Iio 0 ×ˢ Set.univ → (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) x = (fun p => ↑p.fst ^ p.snd) x
[PROOFSTEP]
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
[PROOFSTEP]
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  ContinuousAt.prod_map continuous_ofReal.continuousAt.neg continuousAt_id
[GOAL]
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
[PROOFSTEP]
apply ContinuousAt.mul
[GOAL]
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.fst) ^ x.snd) (x, y)
[PROOFSTEP]
refine' (continuousAt_cpow (Or.inl _)).comp A
[GOAL]
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ 0 < (-↑(x, y).fst, (x, y).snd).fst.re
[PROOFSTEP]
rwa [neg_re, ofReal_re, neg_pos]
[GOAL]
case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => exp (↑π * I * x.snd)) (x, y)
[PROOFSTEP]
exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
have :
  (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) = Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) :=
  by
  ext p
  erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg_of_nonneg p.1.2 _)]
  rfl
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
[PROOFSTEP]
ext p
[GOAL]
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑(p.fst ^ p.snd) = ↑((toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)) p)
[PROOFSTEP]
erw [coe_rpow, Real.coe_toNNReal _ (Real.rpow_nonneg_of_nonneg p.1.2 _)]
[GOAL]
case h.a
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ ↑p.fst ^ p.snd = ↑p.fst ^ ((fun p => (↑p.fst, p.snd)) p).snd
[PROOFSTEP]
rfl
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (x, y)
[PROOFSTEP]
rw [this]
[GOAL]
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)) (x, y)
[PROOFSTEP]
refine' continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp _ _)
[GOAL]
case refine'_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (↑(x, y).fst, (x, y).snd)
[PROOFSTEP]
apply Real.continuousAt_rpow
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
simp only [Ne.def] at h
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : ¬x = 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
rw [← NNReal.coe_eq_zero x] at h
[GOAL]
case refine'_1.h
x : ℝ≥0
y : ℝ
h : ¬↑x = 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ (↑(x, y).fst, (x, y).snd).fst ≠ 0 ∨ 0 < (↑(x, y).fst, (x, y).snd).snd
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p => p.fst ^ p.snd) = toNNReal ∘ (fun p => p.fst ^ p.snd) ∘ fun p => (↑p.fst, p.snd)
⊢ ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
[PROOFSTEP]
exact ((continuous_subtype_val.comp continuous_fst).prod_mk continuous_snd).continuousAt
[GOAL]
x y : ℝ≥0
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
rw [tsub_add_cancel_of_le hy.le] at hm
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
refine' eventually_atTop.2 ⟨m + 1, fun n hn => _⟩
[GOAL]
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
simpa only [NNReal.rpow_one_div_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn), NNReal.rpow_nat_cast] using
  hm.le.trans (pow_le_pow hy.le (m.le_succ.trans hn))
[GOAL]
x : ℝ≥0
y : ℝ
h✝¹ : x ≠ 0 ∨ 0 ≤ y
h✝ : 0 ≤ y
h : 0 = y
⊢ ContinuousAt (fun z => z ^ 0) x
[PROOFSTEP]
simp only [rpow_zero, continuousAt_const]
[GOAL]
x : ℝ≥0∞
hx : x ≠ ⊤
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
lift x to ℝ≥0 using hx
[GOAL]
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
by_cases y = ∞
[GOAL]
case intro
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
by_cases y = ∞
[GOAL]
case pos
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
exact eventually_of_forall fun n => h.symm ▸ le_top
[GOAL]
case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
[PROOFSTEP]
lift y to ℝ≥0 using h
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
have := NNReal.eventually_pow_one_div_le x (by exact_mod_cast hy : 1 < y)
[GOAL]
x y : ℝ≥0
hy : 1 < ↑y
⊢ 1 < y
[PROOFSTEP]
exact_mod_cast hy
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
refine' this.congr (eventually_of_forall fun n => _)
[GOAL]
case neg.intro
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ x ^ (1 / ↑n) ≤ y ↔ ↑x ^ (1 / ↑n) ≤ ↑y
[PROOFSTEP]
rw [coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]
[GOAL]
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
n : ℕ
⊢ 0 ≤ 1 / ↑n
[PROOFSTEP]
positivity
[GOAL]
x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
by_cases hx : x = ⊤
[GOAL]
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
rw [hx, ContinuousAt]
[GOAL]
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ Tendsto (fun a => a ^ y) (𝓝 ⊤) (𝓝 (⊤ ^ y))
[PROOFSTEP]
convert ENNReal.tendsto_rpow_at_top h
[GOAL]
case h.e'_5.h.e'_3
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ⊤ ^ y = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
lift x to ℝ≥0 using hx
[GOAL]
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (fun a => a ^ y) ↑x
[PROOFSTEP]
rw [continuousAt_coe_iff]
[GOAL]
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt ((fun a => a ^ y) ∘ some) x
[PROOFSTEP]
convert continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1
[GOAL]
case h.e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a => a ^ y) ∘ some = some ∘ fun z => z ^ y
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_5.h
y : ℝ
h : 0 < y
x✝ x : ℝ≥0
⊢ ((fun a => a ^ y) ∘ some) x = (some ∘ fun z => z ^ y) x
[PROOFSTEP]
simp [coe_rpow_of_nonneg _ h.le]
[GOAL]
y : ℝ
⊢ Continuous fun a => a ^ y
[PROOFSTEP]
refine continuous_iff_continuousAt.2 fun x => ?_
[GOAL]
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
[GOAL]
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
exact continuousAt_rpow_const_of_pos hy
[GOAL]
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x
[PROOFSTEP]
simp only [rpow_zero]
[GOAL]
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x
[PROOFSTEP]
exact continuousAt_const
[GOAL]
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
have z_pos : 0 < z := by simpa [hz] using hy
[GOAL]
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z
[PROOFSTEP]
simpa [hz] using hy
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x
[PROOFSTEP]
simp_rw [hz, rpow_neg]
[GOAL]
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x
[PROOFSTEP]
exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)
[GOAL]
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)
[PROOFSTEP]
convert ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
[GOAL]
case h.e'_5.h.e'_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 = c * 0 ^ y
[PROOFSTEP]
simp [hy]
[GOAL]
case convert_3
c : ℝ≥0∞
hc : c ≠ ⊤
y : ℝ
hy : 0 < y
⊢ 0 ^ y ≠ 0 ∨ c ≠ ⊤
[PROOFSTEP]
exact Or.inr hc


[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ 0) (↑0 * x ^ (0 - 1)) x
[PROOFSTEP]
simp [hasStrictDerivAt_const]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ 1) (↑1 * x ^ (1 - 1)) x
[PROOFSTEP]
simpa using hasStrictDerivAt_id x
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n✝ n : ℕ
x : 𝕜
⊢ HasStrictDerivAt (fun x => x ^ (n + 1 + 1)) (↑(n + 1 + 1) * x ^ (n + 1 + 1 - 1)) x
[PROOFSTEP]
simpa [pow_succ', add_mul, mul_assoc] using (hasStrictDerivAt_pow (n + 1) x).mul (hasStrictDerivAt_id x)
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
hc : HasDerivAt c c' x
⊢ HasDerivAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
hc : HasDerivWithinAt c c' univ x
⊢ HasDerivWithinAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') univ x
[PROOFSTEP]
exact hc.pow n


[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ HasDerivAtFilter f f' x L ↔ Tendsto (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)
[PROOFSTEP]
simp only [hasDerivAtFilter_iff_tendsto, ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero,
  slope_def_module, smul_sub]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ ∀ (x_1 : 𝕜), ¬x_1 ∈ {x}ᶜ → slope f x x_1 - (x_1 - x)⁻¹ • (x_1 - x) • f' = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') =ᶠ[L ⊓ 𝓟 {x}ᶜ] fun y => slope f x y - f'
[PROOFSTEP]
refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
[PROOFSTEP]
rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')
[PROOFSTEP]
rw [← nhds_translation_sub f', tendsto_comap_iff]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto ((fun x => x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')
[PROOFSTEP]
simp only [HasDerivWithinAt, nhdsWithin, diff_eq, inf_assoc.symm, inf_principal.symm]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')
[PROOFSTEP]
exact hasDerivAtFilter_iff_tendsto_slope
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
hs : ¬x ∈ s
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
[PROOFSTEP]
rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
have hr₀ : 0 < r := lt_of_le_of_lt (norm_nonneg f') hr
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
have A : ∀ᶠ z in 𝓝[s \ { x }] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
  (hasDerivWithinAt_iff_tendsto_slope.1 hf).norm (IsOpen.mem_nhds isOpen_Iio hr)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
have B : ∀ᶠ z in 𝓝[{ x }] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
  mem_of_superset self_mem_nhdsWithin (singleton_subset_iff.2 <| by simp [hr₀])
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ x ∈ {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1}
[PROOFSTEP]
simp [hr₀]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
have C := mem_sup.2 ⟨A, B⟩
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C : {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
rw [← nhdsWithin_union, diff_union_self, nhdsWithin_union, mem_sup] at C
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
[PROOFSTEP]
filter_upwards [C.1]
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
[PROOFSTEP]
simp only [norm_smul, mem_Iio, norm_inv]
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
[PROOFSTEP]
exact fun _ => id
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
[PROOFSTEP]
apply (hf.limsup_norm_slope_le hr).mono
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ ∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
[PROOFSTEP]
intro z hz
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
[PROOFSTEP]
refine' lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) _) hz
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ 0 ≤ ‖z - x‖⁻¹
[PROOFSTEP]
exact inv_nonneg.2 (norm_nonneg _)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
[PROOFSTEP]
have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[Ioi x] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
[PROOFSTEP]
refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[Ioi x] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
[PROOFSTEP]
rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz


[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasStrictDerivAt (↑f) (↑f.linear 1) x
[PROOFSTEP]
rw [f.decomp]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasStrictDerivAt (↑f.linear + fun x => ↑f 0) (↑f.linear 1) x
[PROOFSTEP]
exact f.linear.hasStrictDerivAt.add_const (f 0)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasDerivAtFilter (↑f) (↑f.linear 1) x L
[PROOFSTEP]
rw [f.decomp]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasDerivAtFilter (↑f.linear + fun x => ↑f 0) (↑f.linear 1) x L
[PROOFSTEP]
exact f.linear.hasDerivAtFilter.add_const (f 0)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasStrictDerivAt (↑(lineMap a b)) (b - a) x
[PROOFSTEP]
simpa using (lineMap a b : 𝕜 →ᵃ[𝕜] E).hasStrictDerivAt