mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
d : ℝ
s : Set E
hs : 0 ≤ d
⊢ μH[d] (⇑K.orthogonalProjectionOnto '' s) ≤ μH[d] s

Tactic:
simpa using

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
d : ℝ
s : Set E
hs : 0 ≤ d
⊢ μH[d] (⇑K.orthogonalProjectionOnto '' s) ≤ μH[d] s
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ ?m.187 ∉ closure s

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ ?m.187 ∉ closure s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a b : E
⊢ ⟪a, b⟫ ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a b : E
⊢ ⟪a, b⟫ * ⟪a, b⟫ + (o.areaForm a) b * (o.areaForm a) b = ‖a‖ * ‖a‖ * (‖b‖ * ‖b‖)
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' : u < (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') ((toWeakSpace 𝕜 E) x)
y : E
hy : y ∈ s
⊢ (toWeakSpace 𝕜 E) y ∈ {y | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') y ≤ u}

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' : u < (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') ((toWeakSpace 𝕜 E) x)
y : E
hy : y ∈ s
⊢ RCLike.re (f y) ≤ u
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
⊢ ⇑(toWeakSpace 𝕜 E) '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
refine LinearMap.image_convexHull (toWeakSpace 𝕜 E).toLinearMap s

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜₂ F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜₂ F
inst✝ : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
hAB : (inducingFn σ E F) A = (inducingFn σ E F) B
⊢ ∀ (x : E) (y : F⋆), y (A x) = y (B x)

Tactic:
simpa using

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜₂ F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜₂ F
inst✝ : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
hAB : (inducingFn σ E F) A = (inducingFn σ E F) B
⊢ ∀ (x : E) (y : F⋆), y (A x) = y (B x)
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜₂ F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜₂ F
inst✝ : SeparatingDual 𝕜₂ F
⊢ IsEmbedding ⇑(inducingFn σ E F)

Tactic:
by
  refine Function.Injective.isEmbedding_induced fun A B hAB => ?_
  rw [ContinuousLinearMapWOT.ext_dual_iff]
  simpa [funext_iff] using hAB

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
he' : Continuous fun x ↦ (toWeakSpace 𝕜 F) (e ((toWeakSpace 𝕜 E).symm x))
h_convex : Convex ℝ (⇑e '' s)
⊢ ⇑(toWeakSpace 𝕜 F) '' ⇑e '' closure s ⊆ closure (⇑(toWeakSpace 𝕜 F) '' ⇑e '' s)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E →ₗ[𝕜] F
he : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
he' : Continuous fun x ↦ (toWeakSpace 𝕜 F) (e ((toWeakSpace 𝕜 E).symm x))
h_convex : Convex ℝ (⇑e '' s)
⊢ (fun x ↦ (toWeakSpace 𝕜 F) (e x)) '' closure s ⊆ closure ((fun x ↦ (toWeakSpace 𝕜 F) (e x)) '' s)
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : E
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
A B : E →SWOT[σ] F
⊢ ‖y ((A + B) x)‖ ≤ ‖y (A x)‖ + ‖y (B x)‖

Tactic:
simpa using

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : E
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
A B : E →SWOT[σ] F
⊢ ‖y (A x) + y (B x)‖ ≤ ‖y (A x)‖ + ‖y (B x)‖
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
he₂ : ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)
⊢ ⇑e.symm '' closure (⇑e '' s) ⊆ ⇑e.symm '' ⇑e '' closure s

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
he₂ : ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)
⊢ closure (⇑e '' s) ⊆ ⇑e.symm ⁻¹' closure s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.normSq ((o.kahler x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, y⟫ * ⟪x, y⟫ + (o.areaForm x) y * (o.areaForm x) y = ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
⊢ ‖x‖ * ‖y‖ = 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
⊢ x = 0 ∨ y = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0

Tactic:
simpa using

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0

Tactic:
simpa using

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : StrongDual 𝕜 E), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : StrongDual 𝕜 E), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e_dual f)
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : StrongDual 𝕜 E), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)

Tactic:
simpa using

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : StrongDual 𝕜 E), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e_dual.symm f)
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (-↑x).im ≤ π

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ 0 ≤ π
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : IntegrableOn (fun x ↦ |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (↑σ - 1) • f ((rexp ∘ Neg.neg) x)) univ volume
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ Integrable (fun x ↦ cexp (-↑σ * ↑x) • f (rexp (-x))) volume

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : IntegrableOn (fun x ↦ |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (↑σ - 1) • f ((rexp ∘ Neg.neg) x)) univ volume
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ Integrable (fun x ↦ cexp (-(↑σ * ↑x)) • f (rexp (-x))) volume
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
⊢ Integrable (𝓕 fun u ↦ rexp (-(σ * u)) • f (rexp (-u))) volume

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
⊢ Integrable (𝓕 fun u ↦ rexp (-(σ * u)) • f (rexp (-u))) volume
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
⊢ ContinuousAt f (rexp (- -Real.log x))

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
⊢ ContinuousAt f x
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ↑x ^ ↑(-σ) • rexp (Real.log x * σ) • f (rexp (Real.log x)) = f x

Tactic:
← rpow_def_of_pos hx,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ↑x ^ ↑(-σ) • x ^ σ • f (rexp (Real.log x)) = f x
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
⊢ logTaylor (n + 1) = logTaylor n + fun z ↦ (-1) ^ (n + 1) * z ^ n / ↑n

Tactic:
by
  funext
  simpa only [logTaylor] using! Finset.sum_range_succ ..

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
n : ℕ
ih : logTaylor n 0 = 0
⊢ logTaylor (n + 1) 0 = 0

Tactic:
simpa using

Goal state after:
case succ
n : ℕ
ih : logTaylor n 0 = 0
⊢ ¬n = 0 ∨ n = 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun t ↦ f (t * a)) s = ↑a ^ (-s) • mellin f s

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun t ↦ f (a * t)) s = ↑a ^ (-s) • mellin f s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun z ↦ (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z

Tactic:
have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
      simp_rw [div_eq_mul_inv]
      convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
      simp [field]

Goal state after:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x ↦ x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ HasDerivAt (fun z ↦ (-1) ^ (n + 1 + 1) * (z ^ (n + 1) / (↑n + 1))) ((-1) ^ n * z ^ n) z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ rexp (-x)) =O[atTop] fun x ↦ x ^ (-(s.re + 1))

Tactic:
simpa using

Goal state after:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ rexp (-x)) =O[atTop] fun x ↦ x ^ (-(s.re + 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hsre : -↑0 < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re

Tactic:
simpa using

Goal state after:
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hsre : -↑0 < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hsre : 0 < s.re
this : IsOpen {s | 0 < s.re}
⊢ 0 < s.re

Tactic:
simpa using

Goal state after:
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hsre : 0 < s.re
this : IsOpen {s | 0 < s.re}
⊢ 0 < s.re
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
        mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
this : ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-↑n)
⊢ ContinuousAt Gamma (-↑n)

Tactic:
simpa using

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
this : ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-↑n)
⊢ ContinuousAt Gamma (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun y ↦ -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x

Tactic:
have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
  have b : HasDerivAt (Complex.cos ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_cos (x * (2 * z))) a
  have c := (b.comp_ofReal.div_const (2 * z)).fun_neg
  simp at c ⊢; field_simp at c ⊢; simp only [mul_rotate _ 2 z] at c
  exact c

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y ↦ ↑(cos y)) (-↑(sin x)) x

Tactic:
simpa using

Goal state after:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y ↦ Complex.cos ↑y) (-Complex.sin ↑x) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z) + ∑ i ∈ Finset.range 1, z ^ i / ↑i)

Tactic:
simpa using

Goal state after:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z))