-- Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt {ι : Type*} [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

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : 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

Tactic:
rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i)
    hφ' with
  ⟨Λ, Λ₀, h0, hsum⟩

Result:
case intro.intro.intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : 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 f') x) + Λ₀ • φ' x = 0
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : 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

Tactic:
replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀ := by
  simpa only [funext_iff] using hextr

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : 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

Proof state:
case intro.intro.intro.intro.refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : 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.piRing ℝ ℝ ι ℝ).symm Λ, Λ₀) ≠ 0
hsum : ∀ (x : E), ((LinearEquiv.piRing ℝ ℝ ι ℝ).symm Λ) ((ContinuousLinearMap.pi f') x) + Λ₀ • φ' x = 0
⊢ (Λ, Λ₀) ≠ 0

Tactic:
simpa only [Ne, Prod.ext_iff, LinearEquiv.map_eq_zero_iff, Prod.fst_zero] using h0

Result:
no goals