-- Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt
    (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀)
    (hφ' : HasStrictFDerivAt φ φ' x₀) :
    ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∀ x, Λ (f' x) + Λ₀ • φ' x = 0

Proof state:
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.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
x : E
⊢ Λ (f' x) + Λ₀ • φ' x = (e (Λ, Λ₀) ∘ₗ ↑(f'.prod φ')) x

Tactic:
simp only [e, 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]

Result:
no goals

Proof state:
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 (f'.prod φ') ≤ LinearMap.ker Λ'
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0

Tactic:
set e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  ((LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm).trans
    (LinearMap.coprodEquiv ℝ)

Result:
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 (f'.prod φ') ≤ LinearMap.ker Λ'
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0

Proof state:
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.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0

Tactic:
refine ⟨Λ, Λ₀, e.map_ne_zero_iff.1 h0, fun x => ?_⟩

Result:
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.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
x : E
⊢ Λ (f' x) + Λ₀ • φ' x = 0

Proof state:
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.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
x : E
⊢ Λ (f' x) + Λ₀ • φ' x = 0

Tactic:
convert LinearMap.congr_fun (LinearMap.range_le_ker_iff.1 hΛ') x using 1

Result:
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.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
x : E
⊢ Λ (f' x) + Λ₀ • φ' x = (e (Λ, Λ₀) ∘ₗ ↑(f'.prod φ')) x

Proof state:
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

Tactic:
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Λ'⟩

Result:
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 (f'.prod φ') ≤ LinearMap.ker Λ'
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0