mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case «0»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

pp: case «1»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

pp: case «2»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

pp: case «3»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

pp: case «4»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
<;>

Goal state after:
case «0»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 0) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «1»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 1) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «2»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 2) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «3»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 3) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

case «4»
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hk : 2 * cos (↑r * π) = ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4)
⊢ ↑((Nat.castEmbedding.trans (addLeftEmbedding (-2))) 4) / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

pp: case inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

pp: case inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

pp: case inr.inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

pp: case inr.inr.inr.inr
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

Tactic:
<;>

Goal state after:
case inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inr.inr
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 * π ≤ ↑r * π

pp: case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ≤ 1 * π

Tactic:
<;>

Goal state after:
case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 * π ≤ ↑r * π

case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ≤ 1 * π
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 ≤ ↑r

pp: case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r ≤ 1

Tactic:
<;>

Goal state after:
case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ 0 ≤ ↑r

case hbc
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r ≤ 1
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: case ha
α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ -↑n ≤ -↑m

pp: case hb
α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
<;>

Goal state after:
case ha
α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ -↑n ≤ -↑m

case hb
α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ ↑m ≤ ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).coeff n = (T ℝ ↑n).leadingCoeff

pp: n : ℕ
⊢ (T ℝ ↑n).leadingCoeff = 2 ^ (n - 1)

Tactic:
· simp [leadingCoeff]

Goal state after:
n : ℕ
⊢ (T ℝ ↑n).leadingCoeff = 2 ^ (n - 1)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: case zero
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ 0 ∈ box 0 ↔ 0 = 0

pp: case succ
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ 0 ∈ box (n✝ + 1) ↔ n✝ + 1 = 0

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ 0 ∈ box 0 ↔ 0 = 0

case succ
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ 0 ∈ box (n✝ + 1) ↔ n✝ + 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case zero
L : PeriodPair
l : ℂ
⊢ (if 0 = 0 then ℘[L - l] l else (↑0 + 1) * L.sumInvPow l (0 + 2)) =
    (if 0 = 0 then ℘[L - l] l else ↑(0 + 1)! * L.sumInvPow l (0 + 2)) / ↑0!

pp: case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (if n✝ + 1 = 0 then ℘[L - l] l else (↑(n✝ + 1) + 1) * L.sumInvPow l (n✝ + 1 + 2)) =
    (if n✝ + 1 = 0 then ℘[L - l] l else ↑(n✝ + 1 + 1)! * L.sumInvPow l (n✝ + 1 + 2)) / ↑(n✝ + 1)!

Tactic:
<;>

Goal state after:
case zero
L : PeriodPair
l : ℂ
⊢ (if 0 = 0 then ℘[L - l] l else (↑0 + 1) * L.sumInvPow l (0 + 2)) =
    (if 0 = 0 then ℘[L - l] l else ↑(0 + 1)! * L.sumInvPow l (0 + 2)) / ↑0!

case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (if n✝ + 1 = 0 then ℘[L - l] l else (↑(n✝ + 1) + 1) * L.sumInvPow l (n✝ + 1 + 2)) =
    (if n✝ + 1 = 0 then ℘[L - l] l else ↑(n✝ + 1 + 1)! * L.sumInvPow l (n✝ + 1 + 2)) / ↑(n✝ + 1)!
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z) =o[cofinite] fun n ↦ ↑n

pp: case ho
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑e) =o[cofinite] fun n ↦ ↑n

Tactic:
<;>

Goal state after:
case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z) =o[cofinite] fun n ↦ ↑n

case ho
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑e) =o[cofinite] fun n ↦ ↑n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
n : ℕ
hn : Odd n
⊢ ∑' (l : ↥L.lattice), (↑l ^ n)⁻¹ = -∑' (l : ↥L.lattice), (↑l ^ n)⁻¹

Tactic:
← tsum_neg,

Goal state after:
L : PeriodPair
n : ℕ
hn : Odd n
⊢ ∑' (l : ↥L.lattice), (↑l ^ n)⁻¹ = ∑' (b : ↥L.lattice), -(↑b ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp.e_a.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑k + 1 = ↑(k + 1)

pp: case mp.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑(n - 1) + 1 = ↑n

Tactic:
<;>

Goal state after:
case mp.e_a.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑k + 1 = ↑(k + 1)

case mp.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ ↑(n - 1) + 1 = ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case e'_3
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 x ((⇑derivative)^[k] (T ℝ (-n)))|

pp: case e'_4
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 1 ((⇑derivative)^[k] (T ℝ n)) = eval 1 ((⇑derivative)^[k] (T ℝ (-n)))

Tactic:
<;>

Goal state after:
case e'_3
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 x ((⇑derivative)^[k] (T ℝ (-n)))|

case e'_4
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 1 ((⇑derivative)^[k] (T ℝ n)) = eval 1 ((⇑derivative)^[k] (T ℝ (-n)))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
⊢ fib ↑n = 0 ↔ ↑n = 0

pp: case inr
n : ℕ
⊢ fib (-↑n) = 0 ↔ -↑n = 0

Tactic:
<;>

Goal state after:
case inl
n : ℕ
⊢ fib ↑n = 0 ↔ ↑n = 0

case inr
n : ℕ
⊢ fib (-↑n) = 0 ↔ -↑n = 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
⊢ (fib ↑m).gcd (fib n) = Nat.fib ((↑m).gcd n)

pp: case inr
n : ℤ
m : ℕ
⊢ (fib (-↑m)).gcd (fib n) = Nat.fib ((-↑m).gcd n)

Tactic:
<;>

Goal state after:
case inl
n : ℤ
m : ℕ
⊢ (fib ↑m).gcd (fib n) = Nat.fib ((↑m).gcd n)

case inr
n : ℤ
m : ℕ
⊢ (fib (-↑m)).gcd (fib n) = Nat.fib ((-↑m).gcd n)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl.inl
m n : ℕ
⊢ (fib ↑m).gcd (fib ↑n) = Nat.fib ((↑m).gcd ↑n)

pp: case inl.inr
m n : ℕ
⊢ (fib ↑m).gcd (fib (-↑n)) = Nat.fib ((↑m).gcd (-↑n))

pp: case inr.inl
m n : ℕ
⊢ (fib (-↑m)).gcd (fib ↑n) = Nat.fib ((-↑m).gcd ↑n)

pp: case inr.inr
m n : ℕ
⊢ (fib (-↑m)).gcd (fib (-↑n)) = Nat.fib ((-↑m).gcd (-↑n))

Tactic:
<;>

Goal state after:
case inl.inl
m n : ℕ
⊢ (fib ↑m).gcd (fib ↑n) = Nat.fib ((↑m).gcd ↑n)

case inl.inr
m n : ℕ
⊢ (fib ↑m).gcd (fib (-↑n)) = Nat.fib ((↑m).gcd (-↑n))

case inr.inl
m n : ℕ
⊢ (fib (-↑m)).gcd (fib ↑n) = Nat.fib ((-↑m).gcd ↑n)

case inr.inr
m n : ℕ
⊢ (fib (-↑m)).gcd (fib (-↑n)) = Nat.fib ((-↑m).gcd (-↑n))
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⁻¹ + ∑' (n : ℕ+), ((x - ↑↑n)⁻¹ + (x + ↑↑n)⁻¹)

Tactic:
h0,

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⁻¹ + ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h : MinFacHelper n k
⊢ 1 < n

Tactic:
have : 2 < minFac n := h.1.trans_le h.2.2
  obtain rfl | h := n.eq_zero_or_pos
  · contradiction
  rcases (succ_le_of_lt h).eq_or_lt with rfl | h
  · simp_all
  exact h

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

Goal state before:
pp: case ha
⊢ 0 < 1

pp: case hb
⊢ 0 < √5

Tactic:
<;>

Goal state after:
case ha
⊢ 0 < 1

case hb
⊢ 0 < √5
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.NumberTheory.Real.GoldenRatio

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

pp: case «1»
⊢ (fun n ↦ ↑(Nat.fib n)) 1 = (fun n ↦ (φ ^ n - ψ ^ n) / √5) 1

Tactic:
<;>

Goal state after:
case «0»
⊢ (fun n ↦ ↑(Nat.fib n)) 0 = (fun n ↦ (φ ^ n - ψ ^ n) / √5) 0

case «1»
⊢ (fun n ↦ ↑(Nat.fib n)) 1 = (fun n ↦ (φ ^ n - ψ ^ n) / √5) 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y + (↑n + 1)) ^ (-1 - ↑l)) ℍₒ

pp: case hg
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y - (↑n + 1)) ^ (-1 - ↑l)) ℍₒ

Tactic:
<;>

Goal state after:
case hf
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y + (↑n + 1)) ^ (-1 - ↑l)) ℍₒ

case hg
n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ (y - (↑n + 1)) ^ (-1 - ↑l)) ℍₒ
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 0..M, x ^ k * rexp (-(c * x)) ≤ ↑k ! / c ^ (k + 1)

Tactic:
intervalIntegral.integral_of_le hM

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

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

pp: case e'_4
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), g x ≤ f ↑i
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∑ i ∈ Finset.Ico a b, f ↑i = -∑ i ∈ Finset.Ico a b, (-f) ↑i

Tactic:
<;>

Goal state after:
case e'_3
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), g x ≤ f ↑i
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∫ (x : ℝ) in ↑a..↑b, g x = -∫ (x : ℝ) in ↑a..↑b, (-g) x

case e'_4
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), g x ≤ f ↑i
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∑ i ∈ Finset.Ico a b, f ↑i = -∑ i ∈ Finset.Ico a b, (-f) ↑i
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case ha
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ x₀ ≤ x₀ + ↑k

pp: case hb
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a

Tactic:
<;>

Goal state after:
case ha
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ x₀ ≤ x₀ + ↑k

case hb
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + ↑i ∈ Icc x₀ (x₀ + ↑a)

pp: case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ∈ Icc x₀ (x₀ + ↑a)

pp: case a
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + ↑i ≤ x✝¹

Tactic:
<;>

Goal state after:
case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + ↑i ∈ Icc x₀ (x₀ + ↑a)

case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ∈ Icc x₀ (x₀ + ↑a)

case a
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + ↑i ≤ x✝¹
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Tactic:
by simp only [hf, hab, Nat.cast_sub, add_sub_cancel]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ∈ Icc x₀ (x₀ + ↑a)

pp: case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + (↑i + 1) ∈ Icc x₀ (x₀ + ↑a)

pp: case a
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ≤ x₀ + (↑i + 1)

Tactic:
<;>

Goal state after:
case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ∈ Icc x₀ (x₀ + ↑a)

case x
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + (↑i + 1) ∈ Icc x₀ (x₀ + ↑a)

case a
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x✝¹ ≤ x₀ + (↑i + 1)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₁.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₂.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₃.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₁.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₂.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit
    (ShortComplex.π₃.mapCone
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₁.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₂.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

pp: case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₃.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
<;>

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₁.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₂.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₃.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
intro i hi x hx

Goal state after:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)