case intro.intro.intro
E : Type u_1
F : Type ?u.62036
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
E : Type u_1
F : Type ?u.62036
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
obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ'
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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

case intro.intro.intro.refine'_2
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro
E : Type u_1
F : Type ?u.62036
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
refine' ⟨Λ 1, Λ₀, _, _⟩
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
contrapose! hΛ
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
simp only [Prod.mk_eq_zero] at hΛ ⊢
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
refine' ⟨LinearMap.ext fun x => _, hΛ.2⟩
no goals
case intro.intro.intro.refine'_1
E : Type u_1
F : Type ?u.62036
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
simpa [hΛ.1] using Λ.map_smul x 1
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_2
E : Type u_1
F : Type ?u.62036
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
ext x
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
have H₁ : Λ (f' x) = f' x * Λ 1 := by
  simpa only [mul_one, Algebra.id.smul_eq_mul] using Λ.map_smul (f' x) 1
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
have H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0 := by simpa only [Algebra.id.smul_eq_mul, H₁] using hfΛ x
no goals
case intro.intro.intro.refine'_2.h
E : Type u_1
F : Type ?u.62036
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
simpa [mul_comm] using H₂
no goals
E : Type u_1
F : Type ?u.62036
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
simpa only [mul_one, Algebra.id.smul_eq_mul] using Λ.map_smul (f' x) 1
no goals
E : Type u_1
F : Type ?u.62036
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
simpa only [Algebra.id.smul_eq_mul, H₁] using hfΛ x