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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n

Tactic:
positivity

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

Goal state before:
pp: ⊢ √π ≠ 0

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : √(2 * π * ↑n) * (↑n / rexp 1) ^ n = √π * (√(2 * ↑n) * (↑n / rexp 1) ^ n)
⊢ 0 < √(2 * ↑n) * (↑n / rexp 1) ^ n

Tactic:
positivity

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ 0 ≤ ↑n * π

Tactic:
positivity

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

Goal state before:
pp: case hx
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hy
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

Tactic:
positivity

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

Goal state before:
pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 < √(2 * π * ↑n) * (↑n / rexp 1) ^ n

Tactic:
positivity

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ℕ
⊢ 0 i✝ ≤ (fun i ↦ (↑i + 2) * κ ^ (-↑i)) i✝

Tactic:
positivity

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
⊢ 0 ≤ fun i ↦ (↑i + 2) * κ ^ (-↑i)

Tactic:
intro; positivity

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ↥L.lattice
⊢ 0 i✝ ≤ (fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖) i✝

Tactic:
positivity

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
⊢ 0 ≤ fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖

Tactic:
intro; positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ ↑(Finset.range (n + 1))
⊢ 0 ≤ ↑x * π / ↑n

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 < π

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 < (↑n)⁻¹

Tactic:
positivity

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

Goal state before:
pp: case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ↑((Equiv.prodCongrLeft fun x ↦
            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
          (Prod.map some id p)).2 =
    l₀
⊢ 0 ≤ (↑p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
by
    rw [sumZeroes, mul_eq_zero_iff_left (by aesop)]
    rw [← mul_sum, mul_eq_zero_iff_left (by norm_num)] at this
    simpa [T_real_cos]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
⊢ 0 ≤ π

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ 0 ≤ π / 2

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ 0 ≤ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ z.im ^ 2 ≠ 0

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ 0 < z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.degree = ⊥
⊢ 0 ≠ 2 ^ (n - 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ 0 < z.re ^ 2 + z.im ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 <
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2 +
      1

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 < z.re ^ 2 / z.im ^ 2 + 1

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ 0 ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ π

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 ≤ ‖x‖ ^ (-k)

Tactic:
positivity

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

Goal state before:
pp: case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup
hn : n = 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

Tactic:
simp [hn]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ ↑(Finset.range n)
⊢ 0 ≤ (2 * ↑k + 1) * π / (2 * ↑n)

Tactic:
positivity

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

Goal state before:
pp: case inr
n : ℕ
this :
  ∀ (n : ℕ), n ≠ 0 → (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
hn : n = 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

Tactic:
simp [hn]

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

Goal state before:
pp: n k : ℕ
hk : k ∈ ↑(Finset.range n)
⊢ 0 ≤ (fun k ↦ (↑k + 1) * π / (↑n + 1)) k

Tactic:
positivity

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

Goal state before:
pp: case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
hn : n = 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

Tactic:
simp [hn]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
this : eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0
⊢ 0 < (↑k + 1) * π / (↑n + 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ 0 ≤ ↑(8 * n) * ↑n ^ (-k)

Tactic:
positivity

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ 0 < ↑k * π / ↑n

Tactic:
positivity

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ 0 < ↑k * π / ↑n

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ (if 2 * n = 0 then 1 else 2 * n / (2 * n).gcd (2 * k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
simp [hn]

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
n : ℕ
⊢ 0 < a

Tactic:
positivity

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
if hn0 : n = 0 then simp [hn0] else
    symm
    calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp

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

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'

Tactic:
by rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]

Goal state after:
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:
· simp only [ne_eq, mul_eq_zero, ofReal_eq_zero, not_or]
    exact ⟨Real.pi_ne_zero, integerComplement.ne_zero hz⟩

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

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

Tactic:
positivity

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

Goal state before:
pp: ⊢ φ ≠ 0

Tactic:
positivity

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

Goal state before:
pp: k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
⊢ 0 ≤ ↑k + 1

Tactic:
positivity

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

Goal state before:
pp: k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
⊢ 0 ≤ ↑k + 1

Tactic:
positivity

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

Goal state before:
pp: i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n ↦ ↑(Nat.fib n)) i = (fun n ↦ (φ ^ n - ψ ^ n) / √5) i

Tactic:
fin_cases hi

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.NumberTheory.Real.GoldenRatio

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

Tactic:
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.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ 0 < ↑k + 1

Tactic:
positivity

Goal state after:
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:
positivity

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)
⊢ 0 < log 2 * c

Tactic:
positivity

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

Goal state before:
pp: case hcd
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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := ⋯
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ u (c (N - 1)) ≤ u n

Tactic:
exact hmono cNn

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
n : ℕ
⊢ uIcc (↑N) (↑n + ↑N) ⊆ Ici ↑N

Tactic:
by grind [uIcc_of_le]

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

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ 0 < 1 / j ^ 2

Tactic:
positivity

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
k : ℕ
hk : k ∈ range N
⊢ 0 ≤ c ^ k

Tactic:
positivity

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (a : A), IsConnected (StructuredArrow (L.obj a) R)
this : ∀ (a : Aᵒᵖ), IsConnected (CostructuredArrow R.op (L.op.obj a))
⊢ (fst L R).Final

Tactic:
have : (snd R.op L.op).Initial := initial_snd_of_isConnected_costructuredArrow _ _

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (a : A), IsConnected (StructuredArrow (L.obj a) R)
this✝ : ∀ (a : Aᵒᵖ), IsConnected (CostructuredArrow R.op (L.op.obj a))
this : (snd R.op L.op).Initial
⊢ (fst L R).Final
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ (snd L R).Final

Tactic:
have (a : Aᵒᵖ) : IsCofiltered (CostructuredArrow R.op (L.op.obj a)) :=
    IsCofiltered.of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))
  have : (fst R.op L.op).Initial := initial_fst_of_isCofiltered_costructuredArrow _ _
  have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial :=
    initial_equivalence_comp (opEquiv L R).functor.leftOp _
  have : (snd L R).op.Initial := initial_of_natIso <| opFunctorCompFst _ _
  apply final_of_initial_op

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = y'
⊢ y = y'

Tactic:
let k := IsFiltered.max ky ky'

Goal state after:
case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = y'
k : (i : α) → I i := IsFiltered.max ky ky'
⊢ y = y'
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
⊢ P.isoModSerre 0 ↔ P X ∧ P Y

Tactic:
simp [isoModSerre_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨P, p, q, hp, hq, H⟩ := h

Goal state after:
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ P.isoModSerre (kernel.ι f)

Tactic:
simpa only [isoModSerre_iff_of_mono] using!
      P.prop_of_iso (Abelian.coimageIsoImage f).symm hf

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
by
  have := preservesEpimorphisms L P
  have := Localization.essSurj L P.isoModSerre
  suffices ∀ (W : D) (z : L.obj Y ⟶ W) (hz : L.map f ≫ z = 0),
      ∃ (l : L.obj (cokernel f) ⟶ W), L.map (cokernel.π f) ≫ l = z from
    preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
      ((CokernelCofork.isColimitMapCoconeEquiv _ L).2
        (Cofork.IsColimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (CokernelCofork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_epi] using h₁.trans h₂.symm))))
  intro W w hw
  wlog hw' : ∃ (Z : C) (hZ : L.obj Z = W) (z : Y ⟶ Z), w = L.map z ≫ eqToHom hZ
      generalizing W
  · obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (w ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.map φ.s), Category.assoc,
      MorphismProperty.LeftFraction.map_comp_map_s] at hφ
    obtain ⟨l, hl⟩ := this _ (L.map φ.f) (by rw [← hφ, reassoc_of% hw, zero_comp]) ⟨_, rfl, by simp⟩
    exact ⟨l ≫ inv (L.map φ.s) ≫ (L.objObjPreimageIso W).hom, by simp [reassoc_of% hl, ← hφ]⟩
  obtain ⟨Z, rfl, z, rfl⟩ := hw'
  simp only [eqToHom_refl, Category.comp_id, ← L.map_comp,
    map_eq_zero_iff L P, ← exists_comp_isoModSerre_eq_zero_iff P] at hw
  obtain ⟨Z', t, ht, fac⟩ := hw
  rw [Category.assoc] at fac
  have := Localization.inverts L P.isoModSerre t ht
  exact ⟨L.map (cokernel.desc _ _ fac) ≫ inv (L.map t), by simp [← L.map_comp_assoc]⟩

Goal state after: