mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ angle x 0 = π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle x x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle x (-x) = π

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle (-x) x = π

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' ≤ slope f x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ angle x (r • y) = angle x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ angle (r • x) y = angle x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle x (r • y) = angle x (-y)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle (r • x) y = angle (-x) y

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π) ^ 2 * θ ^ 2 = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) ≤ 2 * (1 - Real.cos θ)

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) = (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ (‖x‖ * ‖y‖) ^ 2

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y ≤ f'

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 0 ≤ |θ|

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2 = 2 * (1 - Real.cos θ)

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - Real.cos θ) ≤ 2 * (1 - (1 - θ ^ 2 / 2))

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - θ ^ 2 / 2)) = θ ^ 2

Tactic:
by

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

Goal state before:
pp: case refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|

Tactic:
rw [Real.sqrt_le_left (by positivity), ← abs_pow, abs_sq]
      calc
        _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
        _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
        _ = _ := by ring

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ MonotoneOn (derivWithin f S) S

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 < π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y ≤ π / 2 * ‖x - y‖

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ MonotoneOn (deriv f) S

Tactic:
by

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

Goal state before:
pp: M : ℝ
z w : ℂ
x✝¹ : M ≠ 0
x✝ : 2 * ↑M - z ≠ 0
h : w = z / (2 * ↑M - z)
⊢ z = 2 * ↑M * w / (1 + w)

Tactic:
by

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

Goal state before:
pp: M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖2 * ↑M * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
by

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ 0 ≤ ‖z‖

Tactic:
by

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ 0 ≤ ‖2 * ↑M - z‖

Tactic:
by

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
this : z.re * z.re ≤ (2 * M - z.re) * (2 * M - z.re)
⊢ ‖z‖ ^ 2 ≤ ‖2 * ↑M - z‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
⊢ sin (angle x (x + y)) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)

Tactic:
by

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ ‖z‖ ≤ ‖2 * ↑M - z‖

Tactic:
by

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
y : ℝ
hy : y ∈ S
hxy : x < y
this : 0 ≤ slope f x y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h : angle x y = π
⊢ angle x z + angle y z = π

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π / 2 ↔ ⟪x, y⟫ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
by

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
y : ℝ
hy : y ∈ S
hyx : y < x
this : slope f x y ≤ 0
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
by

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
⊢ 0 ≤ ‖2 * ↑M - f x‖

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖) ↔ angle x y = π

Tactic:
by

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:
by

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
⊢ ‖f z / (2 * ↑M - f z)‖ ≤ 1 / R * ‖z‖

Tactic:
by

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_rd : derivWithin f (Ioi x) x = 0
⊢ IsMinOn f S x

Tactic:
by

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
⊢ IsMinOn f S x

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
⊢ ?m.101

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h : 2 * ↑M = f z
⊢ False

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' < slope f x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
by
  rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h]
  ring

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ ‖f z‖ = ‖2 * ↑M * w / (1 + w)‖

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y < f'

Tactic:
by

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

Goal state before:
pp: 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₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictMonoOn (derivWithin f S) S

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictMonoOn (deriv f) S

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y ≤ f'

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' ≤ slope f x y

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ ‖2 * ↑M * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 = -(‖x‖ * ‖y‖)

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ AntitoneOn (derivWithin f S) S

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ AntitoneOn (deriv f) S

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y < f'

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 2 * M * (‖w‖ / (1 - ‖w‖)) ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivWithinAt f f' S x
⊢ slope f x y < f'

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivAt f f' x
⊢ slope f x y < f'

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' < slope f x y

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ f' < slope f x y

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) = 2 * M * ‖z‖ / (R - ‖z‖)

Tactic:
by

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

Goal state before:
pp: 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 - 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 : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ ball c r ⊆ ball c R₁

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictAntiOn (derivWithin f S) S

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
⊢ 0 < M + ‖f 0‖

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 = ‖x‖ * ‖y‖

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictAntiOn (deriv f) S

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
⊢ DifferentiableOn ℂ (fun {z} ↦ f z - f 0) (ball 0 R)

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
⊢ f 0 - f 0 = 0

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
hx : x ∈ ball 0 R
⊢ (f x).re - (f 0).re ≤ M - (f 0).re

Tactic:
by

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}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
hx : x ∈ ball 0 R
⊢ M - (f 0).re ≤ M + ‖f 0‖

Tactic:
by

Goal state after: