mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u

Tactic:
have hψ := dfu.tendsto_implicitFunctionOfProdDomain if₂u

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
hψ : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u
Module: Mathlib.Analysis.Calculus.ImplicitContDiff

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
⊢ ContDiffAt 𝕜 n (↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm) (φ.prodFun φ.pt)

Tactic:
← HasStrictFDerivAt.localInverse_def

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
⊢ ContDiffAt 𝕜 n
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    (φ.prodFun φ.pt)
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
this : ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
this : ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u
Module: Mathlib.Analysis.Calculus.ImplicitContDiff

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (f u, u.1)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n (Function.uncurry (⋯.implicitFunctionDataOfProdDomain if₂).implicitFunction) (f u, u.1)
Module: Mathlib.Analysis.Calculus.ImplicitContDiff

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n φ.leftFun φ.pt

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n f u
Module: Mathlib.Analysis.Calculus.ImplicitContDiff

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n φ.rightFun φ.pt

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n Prod.fst u
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : ↑i ≤ n
⊢ iteratedDeriv i (g ∘ f) x = ∑ c, (iteratedFDeriv 𝕜 c.length g (f x)) fun j ↦ iteratedDeriv (c.partSize j) f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ]
  exact iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition hg hf uniqueDiffOn_univ
    uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) hi

Goal state after:
Module: Mathlib.Analysis.Calculus.Implicit

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f').range = ⊤
hker : (↑f').ker.ClosedComplemented
⊢ (f a, 0) ∈ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f').range = ⊤
hker : (↑f').ker.ClosedComplemented
⊢ (f a, 0) ∈ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target
Module: Mathlib.Analysis.Calculus.Implicit

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f').range = ⊤
hker : (↑f').ker.ClosedComplemented
⊢ (f a, 0) ∈ (implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target

Tactic:
simpa only [implicitToOpenPartialHomeomorphOfComplemented_self] using
    (hf.implicitToOpenPartialHomeomorphOfComplemented f f' hf' hker).map_source <|
      hf.mem_implicitToOpenPartialHomeomorphOfComplemented_source hf' hker

Goal state after:
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
hΛ : Λ 1 = 0 ∧ Λ₀ = 0
x : ℝ
⊢ Λ x = 0 x

Tactic:
simpa using

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
hΛ : Λ 1 = 0 ∧ Λ₀ = 0
x : ℝ
⊢ Λ x = 0
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
⊢ Λ (f' x) = f' x * Λ 1

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
⊢ Λ (f' x) = f' x * Λ 1
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
H₁ : Λ (f' x) = f' x * Λ 1
⊢ f' x * Λ 1 + Λ₀ * φ' x = 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
H₁ : Λ (f' x) = f' x * Λ 1
⊢ f' x * Λ 1 + Λ₀ * φ' x = 0
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
H₁ : Λ (f' x) = f' x * Λ 1
H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0
⊢ (Λ 1 • f' + Λ₀ • φ') x = 0 x

Tactic:
simpa using

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
H₁ : Λ (f' x) = f' x * Λ 1
H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0
⊢ f' x * Λ 1 + Λ₀ * φ' x = 0
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
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 ι
⊢ IsLocalExtrOn φ {x | (fun i ↦ f i x) = fun i ↦ f i x₀} x₀

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
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 ι
⊢ IsLocalExtrOn φ {x | ∀ (x_1 : ι), f x_1 x = f x_1 x₀} x₀
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
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
x : E
⊢ (∑ i, Λ i • f' i + Λ₀ • φ') x = 0 x

Tactic:
simpa using

Goal state after:
case refine_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Fintype ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
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
x : E
⊢ ∑ x_1, Λ x_1 * (f' x_1) x + Λ₀ * φ' x = 0
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case intro.refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (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.elim' Λ₀ Λ i • Option.elim' φ' f' i = 0

Tactic:
simpa using

Goal state after:
case intro.refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (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, Λ i • f' i = 0
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ) in f '' s, g x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal |f' x| * g (f x)

Tactic:
simpa using

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ) in f '' s, g x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal |f' x| * g (f x)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ |f' x| • g (f x)) s volume

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ |f' x| • g (f x)) s volume
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case refine_2
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint a (b ∪ c)

Tactic:
simpa using

Goal state after:
case refine_2
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint a (s \ a)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case refine_3
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint b c

Tactic:
simpa using

Goal state after:
case refine_3
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
⊢ Disjoint b (s₁ \ b)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[<] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] a) l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[<] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] a) l
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hf'_nonneg
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ 0 ≤ deriv f z

Tactic:
simpa using

Goal state after:
case hf'_nonneg
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ 0 ≤ f' z