awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
⊢ map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)

Tactic:
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'.prodMk hφ').map_nhds_eq_of_surj htop]
    exact map_snd_nhdsWithin _
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)
⊢ False

Tactic:
hextr.not_nhds_le_map A.ge

Premises used: Eq.ge, IsLocalExtrOn.not_nhds_le_map
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
A : map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)
⊢ False

Tactic:
exact hextr.not_nhds_le_map A.ge

Premises used: Eq.ge, IsLocalExtrOn.not_nhds_le_map
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
rcases :
  ∀ (Λ' : F × ℝ →ₗ[ℝ] ℝ) (h0 : Λ' ≠ 0) (hΛ' : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤ Λ'.ker),
    ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
      (Λ, Λ₀) ≠ 0 ∧
        ∀ (x : E),
          HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
              (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
            0
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) 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Λ'⟩

Premises used: Iff.mpr, Submodule.exists_le_ker_of_lt_top, lt_top_iff_ne_top, IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ' : F × ℝ →ₗ[ℝ] ℝ
h0 : Λ' ≠ 0
hΛ' : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤ Λ'.ker
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
rcases :
  ∀ (Λ : F →ₗ[ℝ] ℝ) (Λ₀ : ℝ)
    (h0 :
      Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ))
    (hΛ' :
      (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
        LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))),
    ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
      (Λ, Λ₀) ≠ 0 ∧
        ∀ (x : E),
          HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
              (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
            0
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0

Tactic:
rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩

Premises used: LinearEquiv.surjective, rfl
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ)
hΛ' :
  (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
    LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0

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

Premises used: And.intro, Exists.intro, Iff.mp, LinearEquiv.map_ne_zero_iff
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ)
hΛ' :
  (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
    LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))
refine :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0

Tactic:
refine ⟨Λ, Λ₀, e.map_ne_zero_iff.1 h0, fun x => ?_⟩
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ)
hΛ' :
  (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
    LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))
x : E
⊢ Eq (α := ℝ)
    (((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) ∘ₗ (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ) : (a : E) → ℝ) x : ℝ)
    ((0 : (a : E) → ℝ) x : ℝ)

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

Premises used: LinearMap.congr_fun, Iff.mp, LinearMap.range_le_ker_iff
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ)
hΛ' :
  (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
    LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))
x : E
h :
  HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
      (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
    ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) ∘ₗ (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ) : (a : E) → ℝ) x
⊢ HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
      (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
    0

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

Premises used: LinearMap.congr_fun, Iff.mp, LinearMap.range_le_ker_iff
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  LinearEquiv.prodCongr (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)) (LinearEquiv.symm (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ)) ≪≫ₗ
    LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : Ne (α := F × ℝ →ₗ[ℝ] ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) : F × ℝ →ₗ[ℝ] ℝ) (0 : F × ℝ →ₗ[ℝ] ℝ)
hΛ' :
  (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range ≤
    LinearMap.ker (R₂ := ℝ) (M₂ := ℝ) (τ₁₂ := RingHom.id ℝ) ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀))
x : E
⊢ HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
      (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
    ((e : (a : (F →ₗ[ℝ] ℝ) × ℝ) → F × ℝ →ₗ[ℝ] ℝ) (Λ, Λ₀) ∘ₗ (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ) : (a : E) → ℝ) x

Tactic:
simp only [e, smul_eq_mul, LinearEquiv.trans_apply, LinearEquiv.prodCongr_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,
    Module.End.one_apply, mul_comm]

Premises used: LinearMap.ringLmapEquivSelf_symm_apply, LinearMap.add_apply, ContinuousLinearMap.coe_coe, LinearEquiv.trans_apply, LinearMap.coprod_comp_prod, Module.End.one_apply, LinearMap.coe_comp, LinearEquiv.prodCongr_apply, LinearMap.coprodEquiv_apply, LinearEquiv.refl_apply, mul_comm, Function.comp_apply, LinearMap.coe_smulRight, smul_eq_mul, ContinuousLinearMap.coe_prod
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
obtain :
  ∀ (Λ : Module.Dual ℝ ℝ) (Λ₀ : ℝ) (hΛ : (Λ, Λ₀) ≠ 0)
    (hfΛ :
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0),
    ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0

Tactic:
obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ'

Premises used: IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0

Tactic:
⟨Λ 1, Λ₀, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
refine_1 : Ne (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)
refine_2 : HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' = 0
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0

Tactic:
refine ⟨Λ 1, Λ₀, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
refine_1 : ∀ (hΛ : Eq (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)), (Λ, Λ₀) = 0
⊢ Ne (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)

Tactic:
contrapose hΛ
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
hΛ : Eq (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)
refine_1 : ∀ (hΛ : Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) (0 : ℝ) ∧ Λ₀ = 0), Λ = 0 ∧ Λ₀ = 0
⊢ (Λ, Λ₀) = 0

Tactic:
simp only [Prod.mk_eq_zero] at hΛ ⊢

Premises used: Prod.mk_eq_zero
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
hΛ : Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) (0 : ℝ) ∧ Λ₀ = 0
⊢ Λ = 0 ∧ Λ₀ = 0

Tactic:
⟨LinearMap.ext fun x => ?_, hΛ.2⟩

Premises used: LinearMap.ext, And.right, And.intro
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
hΛ : Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) (0 : ℝ) ∧ Λ₀ = 0
refine_1 : ∀ (x : ℝ), Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) x : ℝ) ((0 : (a : ℝ) → ℝ) x : ℝ)
⊢ Λ = 0 ∧ Λ₀ = 0

Tactic:
refine ⟨LinearMap.ext fun x => ?_, hΛ.2⟩
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
hΛ : Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) (0 : ℝ) ∧ Λ₀ = 0
x : ℝ
⊢ Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) x : ℝ) ((0 : (a : ℝ) → ℝ) x : ℝ)

Tactic:
simpa [hΛ.1] using Λ.map_smul x 1

Premises used: And.left, LinearMap.map_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
refine_2 :
  ∀ (x : E),
    Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' : (a : E) → ℝ) x : ℝ)
      ((0 : (a : E) → ℝ) x : ℝ)
⊢ HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' = 0

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
⊢ (Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ)

Tactic:
simpa only [mul_one, smul_eq_mul] using Λ.map_smul (f' x) 1

Premises used: LinearMap.map_smul, smul_eq_mul, mul_one, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
⊢ (Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ)

Tactic:
have H₁ : Λ (f' x) = f' x * Λ 1 := by
      simpa only [mul_one, smul_eq_mul] using Λ.map_smul (f' x) 1
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
H₁ :
  (Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) +
      HMul.hMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ) =
    0

Tactic:
simpa only [smul_eq_mul, H₁] using hfΛ x

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
H₁ :
  (Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) +
      HMul.hMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ) =
    0

Tactic:
have H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0 := by simpa only [smul_eq_mul, H₁] using hfΛ x
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ) ((Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) : ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
H₁ :
  (Λ : (a : ℝ) → ℝ) ((f' : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ)
H₂ :
  HMul.hMul (α := ℝ) (β := ℝ) ((f' : (a : E) → ℝ) x : ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) +
      HMul.hMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ) =
    0
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' : (a : E) → ℝ) x : ℝ)
    ((0 : (a : E) → ℝ) x : ℝ)

Tactic:
simpa [mul_comm] using H₂

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (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 : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀

Tactic:
simpa only [funext_iff] using hextr

Premises used: funext_iff