mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
]

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π / 2) ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x

Tactic:
]

Goal state after:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x - ↑π / 2) ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ deriv f a < deriv f b

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ deriv f a < deriv f b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ deriv f a < deriv f b

Tactic:
exact hf'_mono ⟨hxa, hay⟩ ⟨hxa.trans hab, hby⟩ hab

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

Goal state before:
pp: x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x

Tactic:
]

Goal state after:
x : ℂ
⊢ (∃ k, ↑k * (2 * ↑π) = x + ↑π / 2) ↔ ∃ k, -(↑π / 2) + ↑k * (2 * ↑π) = x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z ≠ deriv f w

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z ≠ deriv f w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inl
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)

Tactic:
]

Goal state after:
case inl
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)
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:
←
      add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2),

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 * ↑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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖)

Tactic:
]

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inl
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
l : ℤ
⊢ ¬y = -((2 * ↑l + 1) * ↑π / 2)

Tactic:
]

Goal state after:
case inl
x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
l : ℤ
⊢ ¬y = -((2 * ↑l + 1) * ↑π / 2)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f w ≤ deriv f b

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ deriv f w ≤ deriv f b
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x ↦ ‖f x‖) (closedBall 0 r) x
this : EqOn f (Function.const E (f x)) (ball 0 b)
⊢ EqOn f (Function.const E (Function.const E (f x) 0)) (ball 0 b)

Tactic:
]

Goal state after:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x ↦ ‖f x‖) (closedBall 0 r) x
this : EqOn f (Function.const E (f x)) (ball 0 b)
⊢ EqOn f (Function.const E (Function.const E (f x) 0)) (ball 0 b)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
]

Goal state after:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)

Tactic:
]

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < deriv f a

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hxb : x < b
hba : b < a
⊢ deriv f b < deriv f a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)

Tactic:
]

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

Tactic:
by
  have A : DifferentiableOn ℝ f (Ioo x y) := fun w wmem =>
    (differentiableAt_of_deriv_ne_zero (h w wmem)).differentiableWithinAt
  obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy hf A
  rcases nonempty_Ioo.2 hxa with ⟨b, ⟨hxb, hba⟩⟩
  refine ⟨b, ⟨hxb, hba.trans hay⟩, ?_⟩
  rw [← ha]
  exact hf'_mono ⟨hxb, hba.trans hay⟩ ⟨hxa, hay⟩ hba

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

Goal state before:
pp: x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ (tan x + tanh y * I) / (1 - tan x * (tanh y * I)) = (tan x + tanh y * I) / (1 - tan x * (tanh y * I))

Tactic:
]

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

Goal state before:
pp: E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
]

Goal state after:
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hwU : w ∈ interior U ∨ w ∈ frontier U
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 4 = ε / 4

Tactic:
]

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

Goal state before:
pp: x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - (tan (x / 2) * cos (x / 2)) ^ 2 = (1 - tan (x / 2) ^ 2) * cos (x / 2) ^ 2

Tactic:
]

Goal state after:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - (tan (x / 2) * cos (x / 2)) ^ 2 = (1 - tan (x / 2) ^ 2) * cos (x / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case neg
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * cos (x / 2) ^ 2

Tactic:
]

Goal state after:
case neg
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * cos (x / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
⊢ tan x = 2 * tan (x / 2) / (1 - tan (x / 2) ^ 2)

Tactic:
conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, tan_two_mul]

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

Goal state before:
pp: z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
]

Goal state after:
z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z w : ℂ
⊢ cexp (z * I) ^ 2 + 1 - cexp (z * I) * 2 * w = cexp (z * I) * (cexp (z * I) - 2 * w) + 1

Tactic:
by ring

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

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h : Tendsto (fun x ↦ ↑(∑ i ∈ range x, f i)) atTop (𝓝 ↑l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)

Tactic:
]

Goal state after:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h : Tendsto (fun x ↦ ↑(∑ i ∈ range x, f i)) atTop (𝓝 ↑l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0

Tactic:
]

Goal state after:
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ball w (infDist w (interior U)ᶜ) ⊆ U

Tactic:
]

Goal state after:
case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ball w (infDist w (interior U)ᶜ) ⊆ U
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: ⊢ Function.Surjective sin

Tactic:
by
  intro x
  rcases cos_surjective x with ⟨z, rfl⟩
  exact ⟨z + π / 2, sin_add_pi_div_two z⟩

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
z : ℝ
hz : z ∈ Ioo w y
⊢ deriv f z ≠ deriv f w
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h : Tendsto ((fun z ↦ ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 ↑l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)

Tactic:
]

Goal state after:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h : Tendsto ((fun z ↦ ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 ↑l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ -2 * sin (a / 2) * sin (a * ↑x + b) =
    -2 * sin ((a * (↑(x + 1) - 1 / 2) + b + -(a * (↑x - 1 / 2) + b)) / 2) *
      sin ((a * (↑(x + 1) - 1 / 2) + b - -(a * (↑x - 1 / 2) + b)) / 2)

Tactic:
]

Goal state after:
case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ -2 * sin (a / 2) * sin (a * ↑x + b) =
    -2 * sin ((a * (↑(x + 1) - 1 / 2) + b + -(a * (↑x - 1 / 2) + b)) / 2) *
      sin ((a * (↑(x + 1) - 1 / 2) + b - -(a * (↑x - 1 / 2) + b)) / 2)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h :
  ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z ↦ ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal) x) ↑l < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Set.Iio 1 → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε

Tactic:
]

Goal state after:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 ↑l
h :
  ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z ↦ ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal) x) ↑l < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Set.Iio 1 → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
⊢ ‖f z‖ ≤ C

Tactic:
]

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, sin (a * ↑i + b) = (sin (a / 2) * ∑ i ∈ Finset.range n, sin (a * ↑i + b)) / sin (a / 2)

Tactic:
]

Goal state after:
n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, sin (a * ↑i + b) = (sin (a / 2) * ∑ i ∈ Finset.range n, sin (a * ↑i + b)) / sin (a / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) =
    2 * sin ((a * (↑(x + 1) - 1 / 2) + b - (a * (↑x - 1 / 2) + b)) / 2) *
      cos ((a * (↑(x + 1) - 1 / 2) + b + (a * (↑x - 1 / 2) + b)) / 2)

Tactic:
]

Goal state after:
case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) =
    2 * sin ((a * (↑(x + 1) - 1 / 2) + b - (a * (↑x - 1 / 2) + b)) / 2) *
      cos ((a * (↑(x + 1) - 1 / 2) + b + (a * (↑x - 1 / 2) + b)) / 2)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f w ≤ deriv f b

Tactic:
]

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f w ≤ deriv f b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, cos (a * ↑i + b) = (sin (a / 2) * ∑ i ∈ Finset.range n, cos (a * ↑i + b)) / sin (a / 2)

Tactic:
]

Goal state after:
n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, cos (a * ↑i + b) = (sin (a / 2) * ∑ i ∈ Finset.range n, cos (a * ↑i + b)) / sin (a / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ ((∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x) ↔ ∃ k, ↑k * π = x

Tactic:
]

Goal state after:
x : ℝ
⊢ ((∃ n, ↑n * (2 * π) = x) ∨ ∃ k, π + ↑k * (2 * π) = x) ↔ ∃ k, ↑k * π = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ ((∃ k, π / 2 + ↑k * (2 * π) = x) ∨ ∃ k, -(π / 2) + ↑k * (2 * π) = x) ↔ ∃ k, π / 2 + ↑k * π = x

Tactic:
]

Goal state after:
x : ℝ
⊢ ((∃ k, π / 2 + ↑k * (2 * π) = x) ∨ ∃ k, -(π / 2) + ↑k * (2 * π) = x) ↔ ∃ k, π / 2 + ↑k * π = x
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 D)

Tactic:
]

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 D, 0 ≤ deriv (deriv f) x

Tactic:
]

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.Arctan

Goal state before:
pp: this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = sin x / cos x

Tactic:
]

Goal state after: