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

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) = (1 + z * I) / (1 - z * I)

pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0

Tactic:
]

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
]

Goal state after:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
]

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∃ ε > 0,
    ∀ ⦃y : ℝ⦄,
      dist y 1 < ε →
        y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
]

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∃ ε > 0,
    ∀ ⦃y : ℝ⦄,
      dist y 1 < ε →
        y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ z = z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y ∈ Set.Iio 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
]

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y ∈ Set.Iio 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
]

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1

Tactic:
]

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ -1 < y ∧ y < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : ¬z.re = (↑π / 2).re ∨ ¬z.im = (↑π / 2).im
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ ¬z.re = ((2 * ↑k + 1) * ↑π / 2).re ∨ ¬z.im = ((2 * ↑k + 1) * ↑π / 2).im

Tactic:
]

Goal state after:
z : ℂ
h₀ : ¬z.re = (↑π / 2).re ∨ ¬z.im = (↑π / 2).im
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ ¬z.re = ((2 * ↑k + 1) * ↑π / 2).re ∨ ¬z.im = ((2 * ↑k + 1) * ↑π / 2).im
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ 2) ^ x * y = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Tactic:
]

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ 2) ^ x * y = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
]

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))

Tactic:
]

Goal state after:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2

Tactic:
]

Goal state after:
case inl
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1

Tactic:
]

Goal state after:
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1) + (x - √(x ^ 2 - 1))) / 2 = x

Tactic:
]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1) + (x - √(x ^ 2 - 1))) / 2 = x
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
]

Goal state after:
k : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ x + √(x ^ 2 - 1) = 1 ↔ x = 1

Tactic:
]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ x + √(x ^ 2 - 1) = 1 ↔ x = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
k : ℤ
h₂ : ↑(2 * k + 1) ≤ 1
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2

Tactic:
]

Goal state after:
case inl
z : ℂ
k : ℤ
h₂ : ↑(2 * k + 1) ≤ 1
h₁ : -1 < ↑(2 * k + 1)
nr : z.re = ↑(2 * k + 1) * π / 2
⊢ z.re = π / 2
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k

Tactic:
]

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
k : ℤ
nr : z.re = π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2

Tactic:
]

Goal state after:
case inl
z : ℂ
k : ℤ
nr : z.re = π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
]

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
]

Goal state after:
case e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1) - (x - √(x ^ 2 - 1))) / 2 = √(x ^ 2 - 1)

Tactic:
]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1) - (x - √(x ^ 2 - 1))) / 2 = √(x ^ 2 - 1)
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: ⊢ 𝓝 (π / 2) = 𝓝 (π / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i ↦ (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))

Tactic:
]

Goal state after:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i ↦ (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ √(x ^ 2 - 1) / x = √(x ^ 2 - 1) / x

Tactic:
]

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z

Tactic:
]

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)

Tactic:
]

Goal state after:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ sinh x ^ 2 = sinh x ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ 2 ^ 2 * x * y ≤ (x + y) ^ 2

Tactic:
]

Goal state after:
x y : ℝ≥0
⊢ 2 ^ 2 * x * y ≤ (x + y) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : x ≠ y
this : sqrt (y * x) < (y + x) / 2
hl : ¬y < x
⊢ sqrt (y * x) < (y + x) / 2

Tactic:
]

Goal state after:
case inr
x y : ℝ≥0
h : x ≠ y
this : sqrt (y * x) < (y + x) / 2
hl : ¬y < x
⊢ sqrt (y * x) < (y + x) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ y < x

Tactic:
]

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ y < x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ ¬arcosh x = 0

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬arcosh x = 0
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: n : WithTop ℕ∞
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬↑coshOpenPartialHomeomorph.symm x = 0

Tactic:
]

Goal state after:
n : WithTop ℕ∞
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬↑coshOpenPartialHomeomorph.symm x = 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
]

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ 2 * x * y + 2 * x * y < x ^ 2 + y ^ 2 + 2 * x * y

Tactic:
]

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ 2 * x * y + 2 * x * y < x ^ 2 + y ^ 2 + 2 * x * y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z = z

pp: case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < (2 * (I * z)).im

pp: case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (2 * (I * z)).im ≤ π

Tactic:
]

Goal state after:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < (2 * (I * z)).im

case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ (2 * (I * z)).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2) =
    (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case left
x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y

Tactic:
]

Goal state after:
case left
x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case right
x y : ℝ≥0
h : x ≤ y
⊢ x + y ≤ y + y

Tactic:
]

Goal state after:
case right
x y : ℝ≥0
h : x ≤ y
⊢ x + y ≤ y + y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -(π / 2) < z.re

Tactic:
]

Goal state after:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -(π / 2) < z.re
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - sqrt (x * y)) ≤ dist x y / 2

Tactic:
]

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - sqrt (x * y)) ≤ dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y

Tactic:
]

Goal state after:
case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - (x / 2 + x / 2)) = dist x y / 2

Tactic:
]

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - (x / 2 + x / 2)) = dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑(y - x) / 2 = ↑(y - x) / 2

Tactic:
]

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

Goal state before:
pp: case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z.re ≤ π / 2

Tactic:
]

Goal state after:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z.re ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
⊢ ↑(Real.arctan x) = ↑(Real.arctan x)

pp: case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

pp: case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

pp: case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2

Tactic:
]

Goal state after:
case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case zero
n m : ℕ
x y : ℝ≥0
h : x ≠ y
⊢ (x.agmSequences y 0).1 < (x.agmSequences y 0).2

Tactic:
exact sqrt_mul_lt_half_add_of_ne h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
n✝ m n : ℕ
ih : ∀ {x y : ℝ≥0}, x ≠ y → (x.agmSequences y n).1 < (x.agmSequences y n).2
x y : ℝ≥0
h : x ≠ y
⊢ (x.agmSequences y (n + 1)).1 < (x.agmSequences y (n + 1)).2

Tactic:
agmSequences_succ'

Goal state after:
case succ
n✝ m n : ℕ
ih : ∀ {x y : ℝ≥0}, x ≠ y → (x.agmSequences y n).1 < (x.agmSequences y n).2
x y : ℝ≥0
h : x ≠ y
⊢ (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1 <
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
n✝ m n : ℕ
ih : ∀ {x y : ℝ≥0}, x ≠ y → (x.agmSequences y n).1 < (x.agmSequences y n).2
x y : ℝ≥0
h : x ≠ y
⊢ (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1 <
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2

Tactic:
]

Goal state after:
case succ
n✝ m n : ℕ
ih : ∀ {x y : ℝ≥0}, x ≠ y → (x.agmSequences y n).1 < (x.agmSequences y n).2
x y : ℝ≥0
h : x ≠ y
⊢ (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1 <
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2

Tactic:
]

Goal state after:
case h₀
x : ℝ
⊢ Real.arctan x ≠ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inl
x y : ℝ≥0
h : x ≤ y
⊢ x.agmSequences y = x.agmSequences y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : y ≤ x
⊢ x.agmSequences y = x.agmSequences y

Tactic:
]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0

Tactic:
]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
⊢ -1 < z.re ∨ 1 + z = 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y (n + 1)).1 (x.agmSequences y (n + 1)).2 ≤ dist x y / 2 ^ (n + 1 + 1)

Tactic:
agmSequences_succ'

Goal state after:
case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1
      (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2),
          ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2 ≤
    dist x y / 2 ^ (n + 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1
      (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2),
          ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2 ≤
    dist x y / 2 ^ (n + 1 + 1)

Tactic:
]

Goal state after:
case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).1
      (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2),
          ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2).2 ≤
    dist x y / 2 ^ (n + 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / 2 ^ (n + 1) / 2

Tactic:
]

Goal state after:
case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / 2 ^ (n + 1) / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))

Tactic:
]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))