mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Inverse

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
⊢ derivWithin f s x = 0

Tactic:
by_cases hf : DifferentiableWithinAt 𝕜 f s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Inverse

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
⊢ derivWithin f s x = 0

Tactic:
by_cases hf : DifferentiableWithinAt 𝕜 f s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Tactic:
← image_source_inter_eq,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t ↔ ↑e '' (e.source ∩ s) = e.target ∩ t
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
← contDiffWithinAt_inter hx,

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f (univ ∩ s) x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f (univ ∩ s) x ↔ ContDiffAt 𝕜 n f x

Tactic:
contDiffWithinAt_inter h,

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f univ x ↔ ContDiffAt 𝕜 n f x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
⊢ AnalyticAt 𝕜 f x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticAt 𝕜 f x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffAt 𝕜 n f x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffWithinAt 𝕜 n f univ x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffWithinAt 𝕜 0 f univ x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : Algebra ℚ 𝔸
n : ℕ
⊢ ⇑(expSeries 𝕂 𝔸 n) = ⇑(expSeries ℚ 𝔸 n)

Tactic:
ext c

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : Algebra ℚ 𝔸
n : ℕ
c : Fin n → 𝔸
⊢ (expSeries 𝕂 𝔸 n) c = (expSeries ℚ 𝔸 n) c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (MulOpposite.op x) = MulOpposite.op ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x)

Tactic:
simp_rw [← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (fun x ↦ f x + g x) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ f x + g x) univ x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (fun x ↦ -f x) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ -f x) univ x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x ↦ f i x) x
⊢ ContDiffAt 𝕜 n (fun x ↦ ∑ i ∈ s, f i x) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x ↦ f i x) x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ ∑ i ∈ s, f i x) univ x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (f • g) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (f • g) univ x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
n : ℕ∞ω
R : Type u_3
inst✝² : DistribSMul R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (fun y ↦ c • f y) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
n : ℕ∞ω
R : Type u_3
inst✝² : DistribSMul R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun y ↦ c • f y) univ x
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ closure[inst✝⁵] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]
    simp only [le_of_lt hab, left_mem_Icc]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n : ℕ∞ω
A : Type u_4
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : Module A F
inst✝¹ : IsScalarTower 𝕜 A F
inst✝ : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffAt 𝕜 n f x
v : F
⊢ ContDiffAt 𝕜 n (fun y ↦ f y • v) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n : ℕ∞ω
A : Type u_4
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : Module A F
inst✝¹ : IsScalarTower 𝕜 A F
inst✝ : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffWithinAt 𝕜 n f univ x
v : F
⊢ ContDiffWithinAt 𝕜 n (fun y ↦ f y • v) univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A f L r ε)

Tactic:
rw [Metric.isOpen_iff]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
⊢ ∀ x ∈ A f L r ε, ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: n : ℕ∞ω
x : ℝ
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0

Tactic:
by
  refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩
  have A y (hy : 0 < y) : ContDiffAt ℝ n log y := by
    apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
    · convert! hasDerivAt_exp (log y)
      rw [exp_log hy]
    · exact analyticAt_rexp.contDiffAt
  rcases hx.lt_or_gt with hx | hx
  · have : ContDiffAt ℝ n (log ∘ (fun y ↦ -y)) x := by
      apply ContDiffAt.comp
      · apply A _ (Left.neg_pos_iff.mpr hx)
      apply contDiffAt_id.neg
    convert! this
    ext x
    simp
  · exact A x hx

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
S : Submodule R M := { carrier := ↑C - ↑C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hCS : ↑C ⊆ ↑S
⊢ x ∈ ↑C - ↑C

Tactic:
exact (h ▸ Submodule.span_le.mpr hCS) trivial

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
⊢ C.IsReproducing

Tactic:
rw [IsReproducing, Set.eq_univ_iff_forall]
  intro x
  -- A generating cone in a nontrivial module must be nonempty
  have hne : (C : Set M).Nonempty := Set.nonempty_iff_ne_empty.2 fun h' => by simp [h'] at h
  -- Build the submodule S = C - C and show span C ⊆ S
  let S : Submodule R M := {
    carrier := (C : Set M) - (C : Set M)
    add_mem' := by
      rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨y₁ + y₂, C.add_mem hy₁ hy₂, z₁ + z₂, C.add_mem hz₁ hz₂, add_sub_add_comm ..⟩
    zero_mem' := by
      obtain ⟨c, hc⟩ := hne
      exact ⟨c, hc, c, hc, sub_self c⟩
    smul_mem' := by
      rintro r _ ⟨y, hy, z, hz, rfl⟩
      simp only [Set.mem_sub, SetLike.mem_coe]
      rcases lt_trichotomy r 0 with hr | rfl | hr
      · -- r < 0: use (-r) • z - (-r) • y = r • (y - z)
        refine ⟨(-r) • z, C.smul_mem (neg_pos.mpr hr) hz,
               (-r) • y, C.smul_mem (neg_pos.mpr hr) hy, ?_⟩
        rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]
      · -- r = 0
        simp only [zero_smul]
        obtain ⟨c, hc⟩ := hne
        exact ⟨c, hc, c, hc, sub_self c⟩
      · -- r > 0: use r • y - r • z
        exact ⟨r • y, C.smul_mem hr hy, r • z, C.smul_mem hr hz, (smul_sub r y z).symm⟩}
  have hCS : (C : Set M) ⊆ S := fun x hx ↦
    let ⟨c, hc⟩ := hne; ⟨x + c, C.add_mem hx hc, c, hc, add_sub_cancel_right x c⟩
  exact (h ▸ Submodule.span_le.mpr hCS) trivial

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ HasDerivAt (fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1))
    ((y ^ 2) ^ n / (1 - y ^ 2)) y

Tactic:
by
  refine ((((((hasDerivAt_id _).const_add _).div ((hasDerivAt_id _).const_sub _) (by grind)).log
          ?_).const_mul _).sub (HasDerivAt.fun_sum fun i hi ↦ (hasDerivAt_pow _ _).div_const _))
        |>.congr_deriv ?_
  · simp only [div_ne_zero_iff, Pi.div_apply]; grind
  have : (∑ i ∈ range n, (2 * i + 1) * y ^ (2 * i) / (2 * i + 1)) =
      (∑ i ∈ range n, (y ^ 2) ^ i) := by
    congr with i
    simp [field, mul_comm, ← pow_mul]
  have hy₃ : y ^ 2 ≠ 1 := by simp [hy₁.ne', hy₂.ne]
  have hy₄ : (1 - y) * (1 + y) = 1 - y ^ 2 := by ring
  simp [this, field, geom_sum_eq hy₃, hy₄]
  ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal - ↑ε ≤ (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ).toReal

Tactic:
sub_le_iff_le_add

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ↑(g a) ∂μ).toReal + ↑ε
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖

Tactic:
have k_gt : n e < k := by
      have : ((1 : ℝ) / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1) := lt_trans hk y_lt
      rw [pow_lt_pow_iff_right_of_lt_one₀ (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)] at this
      lia

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
k_gt : n e < k
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case left
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : ε • s ∩ -(ε • s) ∈ 𝓝 0
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x - ε ≤ gauge s (x + y)

Tactic:
sub_le_iff_le_add

Goal state after:
case left
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : ε • s ∩ -(ε • s) ∈ 𝓝 0
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x ≤ gauge s (x + y) + ε
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
⊢ ∃ f, f x < f y

Tactic:
obtain ⟨f, s, t, hs, st, ht⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton
      (convex_singleton y) isClosed_singleton (disjoint_singleton.2 hxy)
  exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩

Goal state after: