awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x
Tactic: have hdg' : ∀ᶠ x in atBot, HasDerivAt g (deriv g x) x :=
    hdg.mono fun _ => DifferentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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₀)
have change : map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p : F × ℝ | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
Tactic: change map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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 (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p : F × ℝ | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
have rw : map Prod.snd (𝓝 (f x₀, φ x₀) ⊓ 𝓟 {p : F × ℝ | p.1 = f x₀}) = 𝓝 (φ x₀)
Tactic: rw [← map_map, nhdsWithin, map_inf_principal_preimage,
      (hf'.prodMk hφ').map_nhds_eq_of_surj htop]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (hypothesis)
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)
⊢ False
have A : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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₀
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0
have 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
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Λ'⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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 ℝ
⊢ ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ),
    (Λ, Λ₀) ≠ 0 ∧
      ∀ (x : E),
        HAdd.hAdd (α := ℝ) ((Λ : (a : F) → ℝ) ((f' : (a : E) → F) x : F) : ℝ)
            (HSMul.hSMul (β := ℝ) Λ₀ ((φ' : (a : E) → ℝ) x : ℝ)) =
          0
have 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
Tactic: rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩
Cleared hypotheses: Λ', h0, hΛ'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
have refine : ∀ (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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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 : ℝ)) =
    0
have 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
Tactic: convert! LinearMap.congr_fun (LinearMap.range_le_ker_iff.1 hΛ') x using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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₀
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
have 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
Tactic: obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
have refine_1 : Ne (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)
Tactic: refine ⟨Λ 1, Λ₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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 : ℝ × ℝ)
⊢ ∃ (a : ℝ) (b : ℝ), (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
have refine_2 : HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' = 0
Tactic: refine ⟨Λ 1, Λ₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
⊢ Ne (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)
have refine_1 : ∀ (hΛ : Eq (α := ℝ × ℝ) (((Λ : (a : ℝ) → ℝ) 1, Λ₀) : ℝ × ℝ) (0 : ℝ × ℝ)), (Λ, Λ₀) = 0
Tactic: contrapose hΛ
Cleared hypotheses: hΛ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
have refine_1 : ∀ (hΛ : Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) (0 : ℝ) ∧ Λ₀ = 0), Λ = 0 ∧ Λ₀ = 0
Tactic: simp only [Prod.mk_eq_zero] at hΛ ⊢
Cleared hypotheses: hΛ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
have refine_1 : ∀ (x : ℝ), Eq (α := ℝ) ((Λ : (a : ℝ) → ℝ) x : ℝ) ((0 : (a : ℝ) → ℝ) x : ℝ)
Tactic: refine ⟨LinearMap.ext fun x => ?_, hΛ.2⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
⊢ HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' = 0
have refine_2 : ∀ (x : E),
  Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' : (a : E) → ℝ) x : ℝ)
    ((0 : (a : E) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (hypothesis)
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
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' : (a : E) → ℝ) x : ℝ)
    ((0 : (a : E) → ℝ) x : ℝ)
have H₁ : (Λ : (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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (hypothesis)
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 : ℝ)
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) ((Λ : (a : ℝ) → ℝ) 1 : ℝ) f' + Λ₀ • φ' : (a : E) → ℝ) x : ℝ)
    ((0 : (a : E) → ℝ) x : ℝ)
have H₂ : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (hypothesis)
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 ι
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
have hextr₁ : 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
Cleared hypotheses: hextr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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₀
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
have 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
Tactic: rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i)
      hφ' with
    ⟨Λ, Λ₀, h0, hsum⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
have 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
Tactic: rcases (LinearEquiv.piRing ℝ ℝ ι ℝ).symm.surjective Λ with ⟨Λ, rfl⟩
Cleared hypotheses: Λ, h0, hsum
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
have refine_1 : (Λ, Λ₀) ≠ 0
Tactic: refine ⟨Λ, Λ₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
⊢ ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
have refine_2 : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
Tactic: refine ⟨Λ, Λ₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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
⊢ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
have refine_2 : ∀ (x : E), Eq (α := ℝ) ((∑ i : ι, Λ i • f' i + Λ₀ • φ' : (a : E) → ℝ) x : ℝ) ((0 : (a : E) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
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₀
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')
have intro : ∀ (val : Fintype ι), ¬LinearIndependent ℝ (Option.elim' φ' f')
Tactic: cases nonempty_fintype ι