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

Goal state before:
pp: case mp.refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMinOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

pp: case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

Tactic:
·

Goal state after:
case mp.refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMinOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ 1 ≤ m + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ AnalyticAt ℂ L.relation x

pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x

Tactic:
·

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ AnalyticAt ℂ L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x

Tactic:
·

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

Tactic:
·

Goal state after:
case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ m + 1 ≤ m + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x

Tactic:
·

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))

Tactic:
simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]

Goal state after:
z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) * I * (1 - cexp (2 * ↑π * I * ↑z))⁻¹) =
    ↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 - cexp (2 * ↑π * I * ↑z))⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℍ
⊢ ↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
have h1 : π * ((exp (2 * π * I * z) + 1) / (I * (1 - exp (2 * π * I * z)))) =
      -π * I * ((exp (2 * π * I * z) + 1) * (1 / (1 - exp (2 * π * I * z)))) := by
    simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]
    ring

Goal state after:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ ↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0

Tactic:
·

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 * (↑n + 1) ^ 2 = - -x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0

Tactic:
·

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ ‖↑s / (↑n + 1) ^ 2‖

pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j

Tactic:
·

Goal state after:
case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ ‖↑s / (↑n + 1) ^ 2‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inr
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))

pp: n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))

Tactic:
·

Goal state after:
case inr
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j

Tactic:
·

Goal state after:
case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
hn : Even n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

pp: case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
·

Goal state after:
case inl
n : ℕ
hn : Even n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case ofNat
n : ℕ
⊢ fib (ofNat n + 2) = fib (ofNat n) + fib (ofNat n + 1)

pp: case negSucc
n : ℕ
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)

Tactic:
·

Goal state after:
case ofNat
n : ℕ
⊢ fib (ofNat n + 2) = fib (ofNat n) + fib (ofNat n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n

pp: case refine_2
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ (n : ℕ), ContinuousOn (fun z ↦ sineTerm z n) Z

Tactic:
·

Goal state after:
case refine_1
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case negSucc
n : ℕ
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)

Tactic:
·

Goal state after:
case negSucc
n : ℕ
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ (n : ℕ), ContinuousOn (fun z ↦ sineTerm z n) Z

Tactic:
·

Goal state after:
case refine_2
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ (n : ℕ), ContinuousOn (fun z ↦ sineTerm z n) Z
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n + 1) * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n + 1))) = fib (-↑(n + n) + 1)

pp: case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1 + 1) * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 + 1))) = fib (-↑(2 * n + 1) + 1)

Tactic:
·

Goal state after:
case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n + 1) * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n + 1))) = fib (-↑(n + n) + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1 + 1) * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 + 1))) = fib (-↑(2 * n + 1) + 1)

Tactic:
·

Goal state after:
case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1 + 1) * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 + 1))) = fib (-↑(2 * n + 1) + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∀ᶠ (n : ℕ) in atTop, DifferentiableOn ℂ (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ

pp: case refine_2
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) / (↑π * x) ≠ 0

Tactic:
·

Goal state after:
case refine_1
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∀ᶠ (n : ℕ) in atTop, DifferentiableOn ℂ (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) / (↑π * x) ≠ 0

Tactic:
·

Goal state after:
case refine_2
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) / (↑π * x) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ (↑π * x).cot * ↑π - 1 / x = ↑π * (↑π * x).cot - 1 / x

pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π ≠ 0

pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0

Tactic:
·

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ (↑π * x).cot * ↑π - 1 / x = ↑π * (↑π * x).cot - 1 / x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π ≠ 0

pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0

Tactic:
·

Goal state after:
case ha
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0

Tactic:
·

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℕ
| fib (-↑m + -↑n) - fib (-↑m + -↑(n + 1))

Tactic:
rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]

Goal state after:
m n : ℕ
| fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1) -
    (fib (-↑m - 1) * fib (-↑(n + 1)) + fib (-↑m) * fib (-↑(n + 1) + 1))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
⊢ fib (↑m + n) = fib (↑m - 1) * fib n + fib ↑m * fib (n + 1)

pp: case inr
n : ℤ
m : ℕ
⊢ fib (-↑m + n) = fib (-↑m - 1) * fib n + fib (-↑m) * fib (n + 1)

Tactic:
·

Goal state after:
case inl
n : ℤ
m : ℕ
⊢ fib (↑m + n) = fib (↑m - 1) * fib n + fib ↑m * fib (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℤ
m : ℕ
⊢ fib (-↑m + n) = fib (-↑m - 1) * fib n + fib (-↑m) * fib (n + 1)

Tactic:
·

Goal state after:
case inr
n : ℤ
m : ℕ
⊢ fib (-↑m + n) = fib (-↑m - 1) * fib n + fib (-↑m) * fib (n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr.inl
m n : ℕ
⊢ fib (-↑m + ↑n) = fib (-↑m - 1) * fib ↑n + fib (-↑m) * fib (↑n + 1)

pp: case inr.inr
m n : ℕ
⊢ fib (-↑m + -↑n) = fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1)

Tactic:
·

Goal state after:
case inr.inl
m n : ℕ
⊢ fib (-↑m + ↑n) = fib (-↑m - 1) * fib ↑n + fib (-↑m) * fib (↑n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr.inr
m n : ℕ
⊢ fib (-↑m + -↑n) = fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1)

Tactic:
·

Goal state after:
case inr.inr
m n : ℕ
⊢ fib (-↑m + -↑n) = fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

pp: case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

pp: case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x

Tactic:
·

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
h : ↑m ∣ n
⊢ fib ↑m ∣ fib n

pp: case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n

Tactic:
·

Goal state after:
case inl
n : ℤ
m : ℕ
h : ↑m ∣ n
⊢ fib ↑m ∣ fib n
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n

Tactic:
·

Goal state after:
case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

pp: case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x

Tactic:
·

Goal state after:
case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x

Tactic:
·

Goal state after:
case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x
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))))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
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:
case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
·

Goal state after:
case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0
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
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0

pp: case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
⊢ 1 < n

Tactic:
·

Goal state after:
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

pp: case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < n.minFac
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n

Tactic:
·

Goal state after:
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
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:
case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z - (↑d + 1))) z
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

pp: case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
·

Goal state after:
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
·

Goal state after:
case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
·

Goal state after:
case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
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) % 2 = 1

pp: case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k + 2 ≤ n.minFac

Tactic:
·

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

Goal state before:
pp: case refine_2.inl
n k' : ℕ
e : n.minFac + 2 = k'
h : MinFacHelper n n.minFac
np : n.minFac ≠ n.minFac
⊢ n.minFac + 2 ≤ n.minFac

pp: case refine_2.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2 : k < n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
·

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

Goal state before:
pp: case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ k + 2 ≤ n.minFac

pp: case refine_2.inr.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ < n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
·

Goal state after:
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ k + 2 ≤ n.minFac
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

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

pp: case e'_5
⊢ -ψ = φ⁻¹

Tactic:
·

Goal state after:
case e'_3
x✝ : ℕ
⊢ ↑(fib x✝) / ↑(fib (x✝ + 1)) = (↑(fib (x✝ + 1)) / ↑(fib x✝))⁻¹
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

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

Tactic:
·

Goal state after:
case e'_5
⊢ -ψ = φ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ 1 < 1 + k

Tactic:
by lia

Goal state after:
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)
Module: Mathlib.NumberTheory.Real.GoldenRatio

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

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

Tactic:
·

Goal state after:
case hu
⊢ fibRec.IsSolution fun n ↦ ↑(Nat.fib n)
Module: Mathlib.NumberTheory.Real.GoldenRatio

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

Tactic:
·

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