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

Goal state before:
pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
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
⊢ ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i

pp: case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
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
⊢ ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
<;>

Goal state after:
case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
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
⊢ ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i

case hbc
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := ⋯
g : ℂ → ℂ := ⋯
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ⋯
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
⊢ ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ ≤ ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n

Tactic:
rw [sub_eq_zero.1 h]

Goal state after:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case hf''.«0»
x : ℝ
hx : 0 < x
hm₀ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 0 ≠ 0
hm₁ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 0 ≠ 1
⊢ False

pp: case hf''.«1»
x : ℝ
hx : 0 < x
hm₀ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 1 ≠ 0
hm₁ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 1 ≠ 1
⊢ False

Tactic:
<;>

Goal state after:
case hf''.«0»
x : ℝ
hx : 0 < x
hm₀ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 0 ≠ 0
hm₁ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 0 ≠ 1
⊢ False

case hf''.«1»
x : ℝ
hx : 0 < x
hm₀ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 1 ≠ 0
hm₁ : (Nat.castEmbedding.trans (addLeftEmbedding 0)) 1 ≠ 1
⊢ False
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ √x * log x) x = (2 + log x) / 0

Tactic:
div_zero

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ √x * log x) x = 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ (2 + log x) / (2 * √x)) x = -log x / 0

Tactic:
div_zero

Goal state after:
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x ↦ (2 + log x) / (2 * √x)) x = 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / 0 = 0

Tactic:
div_zero

Goal state after:
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π + x

pp: case h₂
x y : ℂ
⊢ sin ((x + y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π - x

Tactic:
<;>

Goal state after:
case h₁
x y : ℂ
⊢ sin ((x - y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π + x

case h₂
x y : ℂ
⊢ sin ((x + y) / 2) = 0 ↔ ∃ k, y = 2 * ↑k * ↑π - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

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

pp: case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y

Tactic:
<;>

Goal state after:
case h₁.mp
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) → ∃ k, y = ↑k * ↑π * 2 + x

case h₁.mpr
x y : ℂ
⊢ (∃ k, y = ↑k * ↑π * 2 + x) → ∃ k, x = ↑k * ↑π * 2 + y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

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

Tactic:
· rintro ⟨k, rfl⟩; use -k; simp

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

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

Tactic:
· rintro ⟨k, rfl⟩; use -k; simp

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

Goal state before:
pp: case refine_1
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ↔ y = 2 * ↑k * ↑π + x

pp: case refine_2
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 ↔ y = (2 * ↑k + 1) * ↑π - x

Tactic:
<;>

Goal state after:
case refine_1
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ↔ y = 2 * ↑k * ↑π + x

case refine_2
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 ↔ y = (2 * ↑k + 1) * ↑π - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case refine_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x

pp: case refine_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x

Tactic:
<;>

Goal state after:
case refine_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x

case refine_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case refine_1
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π + (2 * x - ↑π) + ↑π = 2 * (2 * ↑k * ↑π + x)

pp: case refine_2
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π - (2 * x - ↑π) + ↑π = 2 * (↑π * (2 * ↑k + 1) - x)

Tactic:
<;>

Goal state after:
case refine_1
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π + (2 * x - ↑π) + ↑π = 2 * (2 * ↑k * ↑π + x)

case refine_2
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π - (2 * x - ↑π) + ↑π = 2 * (↑π * (2 * ↑k + 1) - x)
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
by
  subst r
  rcases eq_or_ne w z with (rfl | hne); · rfl
  rw [← dist_ne_zero] at hne
  exact norm_max_aux₂ hd (closure_ball z hne ▸ hz.closure hd.continuousOn.norm)

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

Goal state before:
pp: case e'_1.e'_1
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
a✝ : ℤ
⊢ ↑x ≠ (2 * ↑a✝ + 1) * ↑π / 2 ↔ x ≠ (2 * ↑a✝ + 1) * π / 2

pp: case e'_1.e'_2
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
a✝ : ℤ
⊢ ↑y ≠ (2 * ↑a✝ + 1) * ↑π / 2 ↔ y ≠ (2 * ↑a✝ + 1) * π / 2

pp: case e'_2.e'_1
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
x✝ : ℤ
⊢ ↑x = (2 * ↑x✝ + 1) * ↑π / 2 ↔ x = (2 * ↑x✝ + 1) * π / 2

pp: case e'_2.e'_2
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
x✝ : ℤ
⊢ ↑y = (2 * ↑x✝ + 1) * ↑π / 2 ↔ y = (2 * ↑x✝ + 1) * π / 2

Tactic:
<;>

Goal state after:
case e'_1.e'_1
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
a✝ : ℤ
⊢ ↑x ≠ (2 * ↑a✝ + 1) * ↑π / 2 ↔ x ≠ (2 * ↑a✝ + 1) * π / 2

case e'_1.e'_2
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
a✝ : ℤ
⊢ ↑y ≠ (2 * ↑a✝ + 1) * ↑π / 2 ↔ y ≠ (2 * ↑a✝ + 1) * π / 2

case e'_2.e'_1
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
x✝ : ℤ
⊢ ↑x = (2 * ↑x✝ + 1) * ↑π / 2 ↔ x = (2 * ↑x✝ + 1) * π / 2

case e'_2.e'_2
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
x✝ : ℤ
⊢ ↑y = (2 * ↑x✝ + 1) * ↑π / 2 ↔ y = (2 * ↑x✝ + 1) * π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

pp: x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
<;>

Goal state after:
case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hb
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

pp: case hx
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2

pp: x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

pp: x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
<;>

Goal state after:
case hb
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

case hx
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2

x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0

x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case left
⊢ -(π / 2) < π / 4

pp: case right
⊢ π / 4 < π / 2

Tactic:
<;>

Goal state after:
case left
⊢ -(π / 2) < π / 4

case right
⊢ π / 4 < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan ((2⁻¹ + 3⁻¹) / (1 - 2⁻¹ * 3⁻¹)) = π / 4

pp: ⊢ 2⁻¹ * 3⁻¹ < 1

Tactic:
<;>

Goal state after:
⊢ arctan ((2⁻¹ + 3⁻¹) / (1 - 2⁻¹ * 3⁻¹)) = π / 4

⊢ 2⁻¹ * 3⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) = arctan ((1 + 7⁻¹) / (1 - 1 * 7⁻¹))

pp: ⊢ 1 * 7⁻¹ < 1

pp: case h₁
⊢ -1 < 2⁻¹

pp: case h₂
⊢ 2⁻¹ < 1

Tactic:
<;>

Goal state after:
⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) = arctan ((1 + 7⁻¹) / (1 - 1 * 7⁻¹))

⊢ 1 * 7⁻¹ < 1

case h₁
⊢ -1 < 2⁻¹

case h₂
⊢ 2⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan ((2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) + 7⁻¹) / (1 - 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹)) = π / 4

pp: ⊢ 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹ < 1

pp: case h₁
⊢ -1 < 3⁻¹

pp: case h₂
⊢ 3⁻¹ < 1

Tactic:
<;>

Goal state after:
⊢ arctan ((2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) + 7⁻¹) / (1 - 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹)) = π / 4

⊢ 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹ < 1

case h₁
⊢ -1 < 3⁻¹

case h₂
⊢ 3⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) = arctan ((1 + 239⁻¹) / (1 - 1 * 239⁻¹))

pp: ⊢ 1 * 239⁻¹ < 1

pp: case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

pp: case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

pp: case h₁
⊢ -1 < 5⁻¹

pp: case h₂
⊢ 5⁻¹ < 1

Tactic:
<;>

Goal state after:
⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) = arctan ((1 + 239⁻¹) / (1 - 1 * 239⁻¹))

⊢ 1 * 239⁻¹ < 1

case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

case h₁
⊢ -1 < 5⁻¹

case h₂
⊢ 5⁻¹ < 1
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inl
a : ℂ
ha : a ≠ 0
y : ℂ
⊢ angle (a * 0) (a * y) = angle 0 y

pp: case inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * y) = angle x y

Tactic:
<;>

Goal state after:
case inl
a : ℂ
ha : a ≠ 0
y : ℂ
⊢ angle (a * 0) (a * y) = angle 0 y

case inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * y) = angle x y
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inl.inl
a : ℂ
ha : a ≠ 0
⊢ angle (a * 0) (a * 0) = angle 0 0

pp: case inl.inr
a : ℂ
ha : a ≠ 0
y : ℂ
hy : y ≠ 0
⊢ angle (a * 0) (a * y) = angle 0 y

pp: case inr.inl
a : ℂ
ha : a ≠ 0
x : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * 0) = angle x 0

pp: case inr.inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle (a * x) (a * y) = angle x y

Tactic:
<;>

Goal state after:
case inl.inl
a : ℂ
ha : a ≠ 0
⊢ angle (a * 0) (a * 0) = angle 0 0

case inl.inr
a : ℂ
ha : a ≠ 0
y : ℂ
hy : y ≠ 0
⊢ angle (a * 0) (a * y) = angle 0 y

case inr.inl
a : ℂ
ha : a ≠ 0
x : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * 0) = angle x 0

case inr.inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle (a * x) (a * y) = angle x y
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (x * a) (y * a) = angle x y

Tactic:
simp [mul_comm, angle_mul_left ha]

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

Goal state before:
pp: case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Goal state after:
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0

case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Goal state after:
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * ‖0‖) * (⟪x, 0⟫ / (‖x‖ * ‖0‖))) * (‖x‖ * ‖0‖) ^ 2) = √(⟪x, x⟫ * ⟪0, 0⟫ - ⟪x, 0⟫ * ⟪x, 0⟫)

case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
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
  simpa using (hfc.neg.strictMonoOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

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

Goal state before:
pp: case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 → ⟪x, y⟫ = 0

pp: case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ = 0 → ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
<;>

Goal state after:
case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 → ⟪x, y⟫ = 0

case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ = 0 → ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2
⊢ ⟪x, y⟫ = 0

pp: case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
<;>

Goal state after:
case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2
⊢ ⟪x, y⟫ = 0

case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case left
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ π / 2

pp: case right
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ≤ π

Tactic:
<;>

Goal state after:
case left
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ π / 2

case right
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ≤ π
Module: Mathlib.Analysis.Complex.CoveringMap

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

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

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

Tactic:
<;>

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

Goal state before:
pp: case inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
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₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
map_sub

Goal state after:
case inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
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₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z) - g (f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
n : ℕ+
⊢ z ^ n = 0 ↔ z = 0

Tactic:
rw [← coe_inj, coe_pow]
  simp

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this :
  ∀ (n : ℕ),
    ∃ N,
      a ∈ N ∧
        IsOpen[inst✝] N ∧
          ∃ g',
            ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
              p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x✝ : ↑I × A → E
⊢ Set.Icc 0 1 = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
case e'_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this :
  ∀ (n : ℕ),
    ∃ N,
      a ∈ N ∧
        IsOpen[inst✝] N ∧
          ∃ g',
            ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
              p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
x✝ : ↑I × A → E
⊢ ∀ (x : ↑I), x ∈ Set.Icc 0 1
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : ¬(divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : ¬(divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻