mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ (x - (↑n + 1) + (x + (↑n + 1))) / ((x - (↑n + 1)) * (x + (↑n + 1))) = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

pp: case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0

Tactic:
]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ (x - (↑n + 1) + (x + (↑n + 1))) / ((x - (↑n + 1)) * (x + (↑n + 1))) = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun n ↦ (fun n ↦ 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))) n

Tactic:
]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun n ↦ (fun n ↦ 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))) n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))

Tactic:
]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ↑π * (↑π * x).cot - 1 / x = ?m.75

pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ HasSum (fun n ↦ 1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1))) ?m.75

pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ℂ

Tactic:
]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ HasSum (fun n ↦ 1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1))) (↑π * (↑π * x).cot - 1 / x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
h0 : ∑' (n : ℕ+), ((x - ↑↑n)⁻¹ + (x + ↑↑n)⁻¹) = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
h1 : ↑π * (↑π * x).cot - x⁻¹ = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
⊢ ↑π * (↑π * x).cot = x⁻¹ + (↑π * (↑π * x).cot - x⁻¹)

Tactic:
]

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 : ∑' (n : ℕ+), ((x - ↑↑n)⁻¹ + (x + ↑↑n)⁻¹) = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
h1 : ↑π * (↑π * x).cot - x⁻¹ = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
⊢ ↑π * (↑π * x).cot = x⁻¹ + (↑π * (↑π * x).cot - x⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k (fun z ↦ 1 / (z - (↑d + 1))) z + iteratedDeriv k (fun z ↦ 1 / (z + (↑d + 1))) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

pp: case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z - (↑d + 1))) z

pp: case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z

Tactic:
]

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k (fun z ↦ 1 / (z - (↑d + 1))) z + iteratedDeriv k (fun z ↦ 1 / (z + (↑d + 1))) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z - (↑d + 1))) z

case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ (fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)) z + (fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))

Tactic:
]

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ (fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)) z + (fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ -φ < ψ ∧ ψ < φ

Tactic:
]

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ -φ < ψ ∧ ψ < φ
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n (k + 2)

Tactic:
]

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n (k + 2)
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k % 2 = 1

Tactic:
]

Goal state after:
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k % 2 = 1
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ (1 + 1 % 2) % 2 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / (1 - 0)))

Tactic:
]

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / (1 - 0)))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ -ψ = φ⁻¹

Tactic:
]

Goal state after:
⊢ -ψ = φ⁻¹
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
]

Goal state after:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ * ψ = -1

Tactic:
]

Goal state after:
⊢ φ * ψ = -1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1

Tactic:
]

Goal state after:
⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Tactic:
]

Goal state after:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: a : ℕ
h : a % 2 = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k

Tactic:
]

Goal state after:
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: case e'_3
x✝ : ℕ
⊢ ↑(fib x✝) / ↑(fib (x✝ + 1)) = ↑(fib x✝) / ↑(fib (x✝ + 1))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: case e'_5
⊢ -ψ = -ψ

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ - ψ = √5

Tactic:
by ring

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Tactic:
]

Goal state after:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case bc
⊢ 5 < 3 ^ 2

pp: case bc
⊢ 0 < 3

Tactic:
]

Goal state after:
case bc
⊢ 5 < 3 ^ 2

case bc
⊢ 0 < 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ (↑n ^ (1 + k))⁻¹

Tactic:
]

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun n ↦ (↑n ^ (1 + k))⁻¹
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ⁻¹ < 1

Tactic:
]

Goal state after:
⊢ φ⁻¹ < 1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)

Tactic:
]

Goal state after:
β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x ↦ ↑(Nat.fib x)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x ↦ ↑(Nat.fib x)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (X ^ 2 - (X + 1)).IsRoot φ

Tactic:
]

Goal state after:
⊢ (X ^ 2 - (X + 1)).IsRoot φ
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (X ^ 2 - (X + 1)).IsRoot ψ

Tactic:
]

Goal state after:
⊢ (X ^ 2 - (X + 1)).IsRoot ψ
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ Set.EqOn (fun n ↦ ↑(Nat.fib n)) (fun n ↦ (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

pp: case hu
⊢ fibRec.IsSolution fun n ↦ ↑(Nat.fib n)

pp: case hv
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
]

Goal state after:
⊢ Set.EqOn (fun n ↦ ↑(Nat.fib n)) (fun n ↦ (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

case hu
⊢ fibRec.IsSolution fun n ↦ ↑(Nat.fib n)

case hv
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = (√5)⁻¹ * φ ^ x✝ - (√5)⁻¹ * ψ ^ x✝

Tactic:
]

Goal state after:
this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = (√5)⁻¹ * φ ^ x✝ - (√5)⁻¹ * ψ ^ x✝
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (fun n ↦ ↑(Nat.fib n)) = fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
rw [fibRec.eq_iff_eqOn_range_order]
  · intro i hi
    norm_cast at hi
    fin_cases hi <;> simp
  · exact fib_isSol_fibRec
  · suffices LinearRecurrence.IsSolution fibRec
        ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
      convert! this
      rw [Pi.sub_apply]
      ring
    apply (@fibRec ℝ _).solSpace.sub_mem
    · exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenRatio_isSol_fibRec
    · exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenConj_isSol_fibRec

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (fun n ↦ (φ ^ n - ψ ^ n) / √5) = fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ↑(Nat.fib n) = ψ ^ n

Tactic:
]

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ↑(Nat.fib n) = ψ ^ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n

Tactic:
]

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n

Tactic:
]

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
nz : √5 ≠ 0
⊢ (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n ↦ u n / ↑n) '' Ici 1) ≤ u n / ↑n

Tactic:
]

Goal state after:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n ↦ u n / ↑n) '' Ici 1) ≤ u n / ↑n
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) ≤ u n + (↑k * u n + u r)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib n) + φ ^ 2 * ↑(Nat.fib (n + 1)) = φ * (↑(Nat.fib n) + φ * ↑(Nat.fib (n + 1)))

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)

Tactic:
]

Goal state after:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * φ ^ (n + 1) = φ ^ (n + 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
]

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) +
      (-1) ^ k * ↑k ! * (∑' (b : ℕ), (z + (↑b + 1)) ^ (-1 - ↑k) + ∑' (b : ℕ), (z - (↑b + 1)) ^ (-1 - ↑k)) =
    (-1) ^ k * ↑k ! *
      (∑' (n : ℕ), (z + ↑(↑n + 1)) ^ (-1 - ↑k) + (z + ↑0) ^ (-1 - ↑k) + ∑' (n : ℕ), (z + ↑(-(↑n + 1))) ^ (-1 - ↑k))

Tactic:
]

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) +
      (-1) ^ k * ↑k ! * (∑' (b : ℕ), (z + (↑b + 1)) ^ (-1 - ↑k) + ∑' (b : ℕ), (z - (↑b + 1)) ^ (-1 - ↑k)) =
    (-1) ^ k * ↑k ! *
      (∑' (n : ℕ), (z + ↑(↑n + 1)) ^ (-1 - ↑k) + (z + ↑0) ^ (-1 - ↑k) + ∑' (n : ℕ), (z + ↑(-(↑n + 1))) ^ (-1 - ↑k))
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
⊢ Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))

Tactic:
]

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
⊢ Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L

Tactic:
]

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
]

Goal state after:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + iteratedDerivWithin k (fun x ↦ -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))

pp: case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z

pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
]

Goal state after:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + iteratedDerivWithin k (fun x ↦ -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))

case hf
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z

case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ (1 / c) ^ (↑k + 1) * Gamma (↑k + 1) ≠ 0

Tactic:
]

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ (1 / c) ^ (↑k + 1) * Gamma (↑k + 1) ≠ 0
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioc 0 M, x ^ k * rexp (-(c * x)) ∂volume ≤ ↑k ! / c ^ (k + 1)

Tactic:
]

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioc 0 M, x ^ k * rexp (-(c * x)) ∂volume ≤ ↑k ! / c ^ (k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ ((z + ↑n) ^ (k + 1))⁻¹ = ((z + ↑n) ^ (k + 1))⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ (∫ (x : ℝ) in 0..↑M, x ^ k * rexp (-(c * x))) * rexp c ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
]

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ (∫ (x : ℝ) in 0..↑M, x ^ k * rexp (-(c * x))) * rexp c ≤ ↑k ! / c ^ (k + 1) * rexp c
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ↑k ! / c ^ (k + 1) * rexp c = rexp c * ↑k ! / c ^ (k + 1)

Tactic:
by ring

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), 2 ^ (-(c * ↑i)) = rexp (-(log 2 * c) * ↑i)
⊢ 2 ^ c * ↑k ! / (log 2 * c) ^ (k + 1) = 2 ^ c * ↑k ! / (log 2 * c) ^ (k + 1)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)

Tactic:
]

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume

Tactic:
]

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntegrableOn g (Ico ↑i ↑(i + 1)) volume
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g

Tactic:
]

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∫ (x : ℝ) in ↑a..↑b, g x = ∫ (x : ℝ) in ↑a..↑b, g x

pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∀ k ∈ Ico a b, IntervalIntegrable g volume ↑k ↑(k + 1)

Tactic:
]

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∀ k ∈ Ico a b, IntervalIntegrable g volume ↑k ↑(k + 1)