awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀ := by
    simpa only [funext_iff] using hextr
-- 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
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
rcases :
  ∀ (Λ : Module.Dual ℝ ((i : ι) → ℝ)) (Λ₀ : ℝ) (h0 : (Λ, Λ₀) ≠ 0)
    (hsum :
      ∀ (x : E),
        HAdd.hAdd (α := ℝ)
            ((Λ : (a : (i : ι) → ℝ) → ℝ)
                ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
              ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0),
    ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 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⟩

Premises used: Iff.mpr, IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt, hasStrictFDerivAt_pi
-- 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
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ : Module.Dual ℝ ((i : ι) → ℝ)
Λ₀ : ℝ
h0 : (Λ, Λ₀) ≠ 0
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((Λ : (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
rcases :
  ∀ (Λ : ι → ℝ)
    (h0 :
      Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
        (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
          Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
        (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ))
    (hsum :
      ∀ (x : E),
        HAdd.hAdd (α := ℝ)
            ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
                  (a : (i : ι) → ℝ) → ℝ)
                ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
              ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0),
    ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0

Tactic:
rcases (LinearEquiv.piRing ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩

Premises used: LinearEquiv.symm, Real, LinearEquiv.surjective, LinearEquiv.piRing, rfl
-- 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
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 :
  Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
      Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
              (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0

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

Premises used: And.intro, Exists.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
ι : Type u_3
inst_3 : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 :
  Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
      Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
              (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
refine_1 : (Λ, Λ₀) ≠ 0
refine_2 : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0

Tactic:
refine ⟨Λ, Λ₀, ?_, ?_⟩
-- 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
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 :
  Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
      Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
              (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
⊢ (Λ, Λ₀) ≠ 0

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

Premises used: Prod.fst_zero, Prod.ext_iff, Ne, LinearEquiv.map_eq_zero_iff
-- 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
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 :
  Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
      Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
              (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
refine_2 : ∀ (x : E), Eq (α := ℝ) ((∑ i : ι, Λ i • f' i + Λ₀ • φ' : (a : E) → ℝ) x : ℝ) ((0 : (a : E) → ℝ) x : ℝ)
⊢ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 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
ι : Type u_3
inst_3 : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
this : DecidableEq ι := Classical.decEq ι
hextr : IsLocalExtrOn φ {x : E | Eq.{u_3 + 1} (α := (i : ι) → ℝ) (fun (i : ι) ↦ f i x) fun (i : ι) ↦ f i x₀} x₀
Λ₀ : ℝ
Λ : ι → ℝ
h0 :
  Ne (α := Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ, Λ₀) :
      Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
    (0 : Module.Dual ℝ ((i : ι) → ℝ) × ℝ)
hsum :
  ∀ (x : E),
    HAdd.hAdd (α := ℝ)
        ((((LinearEquiv.symm (LinearEquiv.piRing ℝ ℝ ι ℝ) : (a : ι → ℝ) → (ι → ℝ) →ₗ[ℝ] ℝ) Λ : (ι → ℝ) →ₗ[ℝ] ℝ) :
              (a : (i : ι) → ℝ) → ℝ)
            ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ℝ) f' : (a : E) → (i : ι) → ℝ) x : (i : ι) → ℝ) :
          ℝ)
        (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
      0
x : E
⊢ Eq (α := ℝ) ((∑ i : ι, Λ i • f' i + Λ₀ • φ' : (a : E) → ℝ) x : ℝ) ((0 : (a : E) → ℝ) x : ℝ)

Tactic:
simpa [mul_comm] using hsum x

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 : Finite ι
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₀
intro : ∀ (val : Fintype ι), ¬LinearIndependent ℝ (Option.elim' φ' f')
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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 : Finite ι
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₀
val : Fintype ι
intro :
  ¬∀ (g : Option ι → ℝ),
      Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 → ∀ (i : Option ι), g i = 0
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')

Tactic:
rw [Fintype.linearIndependent_iff]

Premises used: Fintype.linearIndependent_iff
-- 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 : Finite ι
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₀
val : Fintype ι
intro :
  ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
⊢ ¬∀ (g : Option ι → ℝ),
      Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 → ∀ (i : Option ι), g i = 0

Tactic:
push Not

Premises used: Not
-- 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 : Finite ι
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₀
val : Fintype ι
intro :
  ∀ (Λ : ι → ℝ) (Λ₀ : ℝ) (hΛ : (Λ, Λ₀) ≠ 0) (hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0),
    ∃ (g : Option ι → ℝ),
      Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0

Tactic:
rcases hextr.exists_multipliers_of_hasStrictFDerivAt hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩

Premises used: IsLocalExtrOn.exists_multipliers_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
ι : Type u_3
inst_3 : Finite ι
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₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0

Tactic:
⟨Option.elim' Λ₀ Λ, ?_, ?_⟩

Premises used: Option.elim', And.intro, Exists.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
ι : Type u_3
inst_3 : Finite ι
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₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
intro : Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i) 0
intro₁ : ∃ (i : Option ι), Option.elim' Λ₀ Λ i ≠ 0
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0

Tactic:
refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩
-- 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 : Finite ι
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₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i) 0

Tactic:
simpa [add_comm] using hΛf

Premises used: add_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 : Finite ι
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₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (i : Option ι), Option.elim' Λ₀ Λ i ≠ 0

Tactic:
simpa only [funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne,
      not_forall] using hΛ

Premises used: funext_iff, Ne, Prod.mk_eq_zero, not_and_or, Option.exists, or_comm, Classical.not_forall
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (μ.prod volume)
hfg :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
h :
  Filter.EventuallyEq.{u_1, u_4} (β := W) (ae μ)
    (fun (a : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f (a, t)) : G →L[ℝ] W) : (a : G) → W) (g' (a, t)))
    fun (a : E) ↦
    -@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (a, t)) : G →L[ℝ] W) : (a : G) → W) (g (a, t))
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f (x, t)) : G →L[ℝ] W) : (a : G) → W) (g' (x, t)) ∂μ)
    (∫ (x : E),
      -@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)) ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (μ.prod volume)
hfg :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
h :
  ∀ (x : E)
    (hf'gx :
      @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
        (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume)
    (hfg'x :
      @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
        (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume)
    (hfgx :
      @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
        (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume),
    Eq.{u_4 + 1} (α := W)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f (x, t)) : G →L[ℝ] W) : (a : G) → W) (g' (x, t)))
      (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)))
⊢ Filter.EventuallyEq.{u_1, u_4} (β := W) (ae μ)
    (fun (a : E) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f (a, t)) : G →L[ℝ] W) : (a : G) → W) (g' (a, t)))
    fun (a : E) ↦
    -@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (a, t)) : G →L[ℝ] W) : (a : G) → W) (g (a, t))

Tactic:
filter_upwards [hf'g.prod_right_ae, hfg'.prod_right_ae, hfg.prod_right_ae]
      with x hf'gx hfg'x hfgx

Premises used: MeasureTheory.Integrable.prod_right_ae
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (μ.prod volume)
hfg :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
apply :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_2 : ℝ) ↦ g (x, x_2)) x_1 →
      HasDerivAt (fun (x_2 : ℝ) ↦ f (x, x_2)) (f' (x, x_1)) x_1
apply₁ :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_2 : ℝ) ↦ f (x, x_2)) x_1 →
      HasDerivAt (fun (x_2 : ℝ) ↦ g (x, x_2)) (g' (x, x_1)) x_1
⊢ Eq.{u_4 + 1} (α := W)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f (x, t)) : G →L[ℝ] W) : (a : G) → W) (g' (x, t)))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)))

Tactic:
apply integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable ?_ ?_ hfg'x hf'gx hfgx

Premises used: MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable