mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, f a ∂μ - ∫ (a : α) in s, g a ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x))

Tactic:
refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)

Goal state after:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c : ℝ
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x =ᶠ[𝓝[<] x] (fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
⊢ ∃ r, 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖

Tactic:
rcases Metric.mem_nhds_iff.1 I with ⟨r, r_pos, hr⟩
    exact ⟨r, r_pos, fun t ht v hv ↦ hr (mem_ball_zero_iff.2 ht) v hv⟩

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

Tactic:
obtain ⟨w, ρ, w_mem, hvw, hρ⟩ : ∃ w ρ, w ∈ sphere 0 1 ∧ v = ρ • w ∧ ρ = ‖v‖ := by
    refine ⟨‖v‖⁻¹ • v, ‖v‖, by simp [norm_smul, inv_mul_cancel₀ (norm_ne_zero_iff.2 v_ne)], ?_, rfl⟩
    simp [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 v_ne)]

Goal state after:
case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case succ.inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
⊢ (fun x ↦ f x - taylorWithinEval f (n + 1) s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ (n + 1)

Tactic:
convert!
      Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
        f x - taylorWithinEval f (n + 1) s x₀ x) using 1

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
⊢ (fun x ↦ f x - taylorWithinEval f (n + 1) s x₀ x) = fun x ↦
    f x - taylorWithinEval f (n + 1) s x₀ x - (f x₀ - taylorWithinEval f (n + 1) s x₀ x₀)

case succ.inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
⊢ ∀ x ∈ s,
    HasDerivWithinAt (fun x ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
      (derivWithin f s x - taylorWithinEval (derivWithin f s) n s x₀ x) s x
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n) f s
h_isLittleO : Filter.Tendsto (fun x ↦ ‖f x - taylorWithinEval f n s x₀ x‖ / ‖(x - x₀) ^ n‖) (𝓝[s] x₀) (𝓝 0)
⊢ Filter.Tendsto (fun x ↦ ‖((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)‖) (𝓝[s] x₀) (𝓝 0)

Tactic:
simpa [norm_smul, div_eq_inv_mul] using h_isLittleO

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: case inr
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ interior (closedBall z r)

Tactic:
exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Convex

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2

Tactic:
hx,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (1 * 1 + ‖y‖ * ‖y‖) - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mp
y : ℂ
k : ℤ
⊢ ∃ k_1, y = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + y)

Tactic:
use -k

Goal state after:
case h
y : ℂ
k : ℤ
⊢ y = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁.mpr
x : ℂ
k : ℤ
⊢ ∃ k_1, x = ↑k_1 * ↑π * 2 + (↑k * ↑π * 2 + x)

Tactic:
use -k

Goal state after:
case h
x : ℂ
k : ℤ
⊢ x = ↑(-k) * ↑π * 2 + (↑k * ↑π * 2 + x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))

Tactic:
hx,

Goal state after:
case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (0 + tan ((2 * ↑l + 1) * ↑π / 2)) / (1 - 0 * tan ((2 * ↑l + 1) * ↑π / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) = 0

Tactic:
mul_div_assoc,

Goal state after:
case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * (↑π / 2) + (2 * ↑l + 1) * ↑π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * (↑π / 2) + (2 * ↑l + 1) * ↑π / 2) = 0

Tactic:
mul_div_assoc,

Goal state after:
case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1) * (↑π / 2) + (2 * ↑l + 1) * (↑π / 2)) = 0
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c

Tactic:
have h3 : IsLocalMax (norm ∘ f⁻¹) c := by refine h2.congr (Eventually.of_forall ?_); simp

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : E → ℂ
c : E
hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMin (norm ∘ f) c
h : ¬f c = 0
h1 : ∀ᶠ (z : E) in 𝓝 c, f z ≠ 0
h2 : IsLocalMax (norm ∘ f)⁻¹ c
h3 : IsLocalMax (norm ∘ f⁻¹) c
⊢ ∀ᶠ (z : E) in 𝓝 c, f z = f c
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ DifferentiableOn ℝ (deriv f) (interior D)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ∀ x ∈ interior D, 0 ≤ deriv (deriv f) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case mp.inr
x : ℝ
n : ℤ
h : -(π / 2) + ↑n * (2 * π) = x
⊢ ∃ k, π / 2 + ↑k * π = x

Tactic:
exact ⟨-1 + n * 2, by grind⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ DifferentiableOn ℝ (deriv f) (interior D)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ∀ x ∈ interior D, deriv (deriv f) x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 * (π / 2) ≤ (2 * ↑r + 1) * π / 2

Tactic:
mul_div_assoc,

Goal state after:
case inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 * (π / 2) ≤ (2 * ↑r + 1) * (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ (2 * ↑r + 1) * π / 2 ≤ -(1 * (π / 2))

Tactic:
mul_div_assoc,

Goal state after:
case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ (2 * ↑r + 1) * (π / 2) ≤ -(1 * (π / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : -(π / 2) ≤ x
hx₀ : x ≤ 0
⊢ sin x ≤ 2 / π * x

Tactic:
by
  simpa using mul_le_sin (neg_nonneg.2 hx₀) (neg_le.2 hx)

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 < deriv (deriv f) x

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x
⊢ ∀ x ∈ interior D, 0 < deriv (deriv f) x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x < 0

Tactic:
interior_interior

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0
⊢ ∀ x ∈ interior D, deriv (deriv f) x < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * π / 2
ub : arctan x < π / 2
⊢ False

Tactic:
mul_div_assoc,

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * (π / 2)
ub : arctan x < π / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * π / 2 < 1 * (π / 2)
⊢ False

Tactic:
mul_div_assoc,

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * (π / 2) < 1 * (π / 2)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
⊢ x < tan x

Tactic:
by
  let U := Ico 0 (π / 2)
  have intU : interior U = Ioo 0 (π / 2) := interior_Ico
  have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
  have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
    exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
  have sin_pos {y : ℝ} (hy : y ∈ interior U) : 0 < sin y := by
    rw [intU] at hy
    exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
  have tan_cts_U : ContinuousOn tan U := by
    apply ContinuousOn.mono continuousOn_tan
    intro z hz
    simp only [mem_ofPred_eq]
    exact (cos_pos hz).ne'
  have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
  have deriv_pos (y : ℝ) (hy : y ∈ interior U) : 0 < deriv (fun y' : ℝ => tan y' - y') y := by
    have := cos_pos (interior_subset hy)
    simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
    norm_cast
    have bd2 : cos y ^ 2 < 1 := by
      apply lt_of_le_of_ne y.cos_sq_le_one
      rw [cos_sq']
      simpa only [Ne, sub_eq_self, sq_eq_zero_iff] using (sin_pos hy).ne'
    rwa [lt_inv_comm₀, inv_one]
    · exact zero_lt_one
    simpa only [sq, mul_self_pos] using this.ne'
  have mono := strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
  have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
  have x_in_U : x ∈ U := ⟨h1.le, h2⟩
  simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1

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

Goal state before:
pp: ⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Tactic:
show 4 * arctan _ = 2 * (2 * _) by ring,

Goal state after:
⊢ 2 * (2 * arctan 5⁻¹) - arctan 239⁻¹ = π / 4
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (⟪0, x⟫ / (‖0‖ * ‖x‖)) = π / 2

Tactic:
rw [inner_zero_left, zero_div, Real.arccos_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
x : ℂ
hx : x ∈ ball 0 R
⊢ f x / (2 * ↑M - f x) ∈ closedBall (f 0 / (2 * ↑M - f 0)) 1

Tactic:
· simpa [hf₂] using
      div_le_one_of_le₀ (norm_le_norm_two_mul_sub hM (hf₁ hx)) (by positivity)

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
⊢ IsMinOn f S x

Tactic:
intro y hy
  rcases lt_trichotomy x y with hxy | h_eq | hyx
  · suffices 0 ≤ slope f x y by
      simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this
      exact this.1
    exact hf_rd.trans <| rightDeriv_le_slope_of_mem_interior hf hx hy hxy
  · simp [h_eq]
  · suffices slope f x y ≤ 0 by
      simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hyx, and_false, or_false] at this
      exact this.1
    rw [slope_comm]
    exact (slope_le_leftDeriv_of_mem_interior hf hy hx hyx).trans hf_ld

Goal state after:
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
suffices ∀ᶠ r in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1) by
      refine ge_of_tendsto ?_ this
      refine ContinuousAt.continuousWithinAt ?_
      fun_prop (disch := positivity)

Goal state after:
case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ ↑n, ⋯⟩

Tactic:
convert! isCoveringMap_npow n _

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
x✝ : { x // x ≠ 0 }
⊢ ↑x✝ ^ ↑n = ↑x✝ ^ n

case inl.convert_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ ProperSpace 𝕜

case inl.convert_4
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := ⋯
x✝ : 𝕜
⊢ x✝ ≠ 0 ↔ x✝ ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
simp [NeZero.ne]

Goal state after:
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ↑n ≠ 0

Tactic:
simp [NeZero.ne]

Goal state after:
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ContinuousOn (U.piecewise (fun x ↦ cexp (f x / ↑n)) fun x ↦ g x ^ (1 / ↑n)) U

Tactic:
rw [continuousOn_iff_continuous_domRestrict, domRestrict_piecewise,
      ← continuousOn_iff_continuous_domRestrict]
    fun_prop

Goal state after: