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

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val.Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: case zero
ι : 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
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ 0 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ 0 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ iteratedDerivWithin 0 (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin 0 (f n) s x

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
this : 7 ≤ meromorphicOrderAt L.relation 0 + ↑6 * meromorphicOrderAt id 0
⊢ 6 ≠ ⊤

Tactic:
simp

Goal state after:
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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
x✝ : ι
⊢ iteratedDerivWithin m (fun z ↦ f x✝ z) s r = iteratedDerivWithin m (fun z ↦ f x✝ z) s r

Tactic:
simp

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

Goal state before:
pp: 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
this : eval x (T ℝ ↑n) ≤ eval (cos (1 * π / ↑n)) (T ℝ ↑n)
⊢ Odd 1 ∧ cos (1 * π / ↑n) = cos (↑1 * π / ↑n)

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation (↑x - ↑x)
a : ℂ
⊢ L.relation a = (L.relation ∘ fun x_1 ↦ x_1 - ↑x) a

Tactic:
simp

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

Goal state before:
pp: 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
⊢ cos (0 * π / ↑n) ∈ Set.Icc (-1) 1

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z : ℂ
w : ↥L.lattice
⊢ L.relation (z + ↑w) = L.relation z

Tactic:
simp

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

Goal state before:
pp: L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
⊢ 0 ∈ L.lattice

Tactic:
simp

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

Goal state before:
pp: 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
this : eval (cos (0 * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)
⊢ 0 ≤ n

Tactic:
simp

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

Goal state before:
pp: 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
this : eval (cos (0 * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)
⊢ Even 0 ∧ cos (0 * π / ↑n) = cos (↑0 * π / ↑n)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
⊢ arithGeom a b u₀ 0 = a ^ 0 * u₀ + b * ∑ k ∈ Finset.range 0, a ^ k

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
⊢ arithGeom a b u₀ 0 = a ^ 0 * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
simp

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
⊢ Nat.Coprime 2 (2 * k + 1)

Tactic:
simp

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
this : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ 2 * k + 1 ≠ 0

Tactic:
simp

Goal state after:
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:
· filter_upwards with n z hz using hu2 n z hz

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) ^ (2 * n) * (-1) ^ 1 * (↑(Nat.fib (2 * n)) - ↑(Nat.fib (2 * n - 1) + Nat.fib (2 * n))) =
    (-1) ^ (2 * n) * ↑(Nat.fib (2 * n - 1))

Tactic:
simp

Goal state after:
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) ^ 1 * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 - 1) + Nat.fib (2 * n + 1))) =
    (-1) ^ (2 * n + 1 - 1 + 1) * ↑(Nat.fib (2 * n + 1 - 1))

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: x✝ : ℤ
⊢ fib (↑0 + x✝) = fib (↑0 - 1) * fib x✝ + fib ↑0 * fib (x✝ + 1)

Tactic:
simp

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

Goal state before:
pp: x✝ : ℤ
⊢ fib (x✝ + ↑0) = fib (x✝ - 1) * fib ↑0 + fib x✝ * fib (↑0 + 1)

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: x✝ : ℕ
⊢ fib (-↑x✝ + -↑0) = fib (-↑x✝ - 1) * fib (-↑0) + fib (-↑x✝) * fib (-↑0 + 1)

Tactic:
simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
i : ℝ[X]
hi✝ : i ∈ f.support
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
hi : T ℝ ↑m = i
⊢ f (T ℝ ↑m) • 1 ≤ f (T ℝ ↑m) • eval 1 (T ℝ ↑m)

Tactic:
simp

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

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ 0 ≤ fib ↑m

Tactic:
simp

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

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ 0 ≤ ↑m

Tactic:
simp

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

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

Tactic:
by
  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.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3

Tactic:
simp

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

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1

Tactic:
simp

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)
⊢ 1 - 0 ≠ 0

Tactic:
simp

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

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = ↑0.5 * (↑1 + √↑5)

Tactic:
simp

Goal state after:
this✝ : Irrational √↑5
this : Irrational (↑1 + √↑5)
⊢ φ = 0.5 * (1 + √5)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = ↑0.5 * (↑1 - √↑5)

Tactic:
simp

Goal state after:
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = 0.5 * (1 - √5)
Module: Mathlib.NumberTheory.Real.GoldenRatio

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ φ * ↑(Nat.fib (0 + 1)) + ↑(Nat.fib 0) = φ ^ (0 + 1)

Tactic:
simp

Goal state after:
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) = ↑(k + 1) * u n + u r

Tactic:
simp

Goal state after:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = (↑k + 1) * u n + u r
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)
⊢ ((fun n ↦ u n / ↑n) '' Ici 1).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

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

Tactic:
simp

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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
⊢ (image (fun i ↦ c i) (range (a + 1))).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (StarSubalgebra.centralizer ℂ ↑S).carrier.centralizer.centralizer = (StarSubalgebra.centralizer ℂ ↑S).carrier

Tactic:
simp

Goal state after:
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
⊢ ↑i ≤ ↑(i + 1)

Tactic:
simp

Goal state after:
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)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i = ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), f ↑i

Tactic:
simp

Goal state after:
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)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ ↑i ≤ ↑(i + 1)

Tactic:
simp

Goal state after:
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)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntervalIntegrable (fun u ↦ f ↑i) volume ↑i ↑(i + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑S.commutant.commutant = ↑S

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ x₀ = x₀ + ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: 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₀ + ↑i ≤ x₀ + (↑i + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i) = ∑ i ∈ Finset.range a, f (x₀ + ↑i)

Tactic:
simp

Goal state after:
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
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
k₂ : A ⟶ Y
hk : k₁ ≫ f = k₂ ∧ k₂ ≫ g = 0
⊢ ((k₁ ≫ biprod.inl + k₂ ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0

Tactic:
obtain ⟨rfl, hk⟩ := hk

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk : (k₁ ≫ f) ≫ g = 0
⊢ ((k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ≫ f ≫ g = 0
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f (↑a + ↑x)

Tactic:
exact AntitoneOn.integral_le_sum (by simp only [hf, hab, Nat.cast_sub, add_sub_cancel])

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1)) = ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
k₂ : A ⟶ Y
hk✝ : (k₁ ≫ biprod.inl + k₂ ≫ biprod.inr) ≫ φ f g = 0
hk : k₁ ≫ f = k₂ ∧ k₂ ≫ g = 0
⊢ kernel.lift (f ≫ g) ((k₁ ≫ biprod.inl + k₂ ≫ biprod.inr) ≫ biprod.fst) ⋯ ≫ ι f g = k₁ ≫ biprod.inl + k₂ ≫ biprod.inr

Tactic:
obtain ⟨rfl, hk⟩ := hk

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
A : C
k₁ : A ⟶ X
hk✝ : (k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ φ f g = 0
hk : (k₁ ≫ f) ≫ g = 0
⊢ kernel.lift (f ≫ g) ((k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr) ≫ biprod.fst) ⋯ ≫ ι f g =
    k₁ ≫ biprod.inl + (k₁ ≫ f) ≫ biprod.inr
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 𝟙 X ≫ f ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g) ≫ 𝟙 Z = f ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫ biprod.snd = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).L₁.g = 𝟙 (snakeInput f g).L₀.X₃ ≫ (snakeInput f g).v₀₁.τ₃

Tactic:
simp

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
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)
⊢ (image (fun i ↦ c i) (range (a + 1))).Nonempty

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ kernel.ι p ≫ p = 0

Tactic:
simp

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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
⊢ ∃ ε, d + ε * (1 + l) < l ∧ 0 < ε

Tactic:
by
      have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ (ConcreteCategory.hom ((((evaluation K (Type w)).obj k).mapCocone t).ι.app j)) y =
    (ConcreteCategory.hom ((t.ι.app j).app k)) y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ ∀ (j : J),
    colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫
        colimMap (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))) ≫
          (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
            (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
      colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫ colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
intro j

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫
      colimMap (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))) ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫ colimit.post F (coyoneda.obj (op (yoneda.obj X)))