[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Λ
