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

Goal state before:
pp: case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
exact (hasDerivAt_arcsin h.1 h.2).deriv

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‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (℘[L - l₀] z)

Tactic:
refine (Summable.hasSum_iff ?_).mpr (L.weierstrassPExcept_eq_tsum l₀ z x hx).symm
  simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]
  exact (L.summable_weierstrassPExceptSummand l₀ z x hx).prod

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) - #(Icc (-↑n) ↑n) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
snd_add,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc ((-1).2 + (-↑n).2) ((↑n).2 + 1.2)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
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
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
have 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 := by ring

Goal state after:
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
⊢ r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
have h11 : x 0 * (z : ℂ) + x 1 = (x 0 / ‖x‖ * z + x 1 / ‖x‖) * ‖x‖ := by
    rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖
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 ≤ k

Tactic:
← Int.cast_nonneg_iff (R := ℝ),

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)

Tactic:
have : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s := by
      by_cases 1 ≤ i ∧ i ≤ n - k
      case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
      case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩

Goal state after:
case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
this : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
← Real.mul_rpow (r_pos _).le (norm_nonneg _)

Goal state after:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
field_simp

Goal state after:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ ↑(Finset.range n)
⊢ 2 * ↑k + 1 ≤ 2 * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
field_simp

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
⊢ ↑↑n * (2 * ↑k + 1) = ↑n * (2 * ↑↑k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos ((2 * ↑k + 1) * π / (2 * ↑n))) (T ℝ ↑n) = 1

Tactic:
rw [← count_roots, roots_T_real, Multiset.count_eq_one_of_mem (by simp)]
  grind

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

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

Tactic:
field_simp

Goal state after:
case h
n k : ℕ
hk : k ∈ ↑(Finset.range n)
⊢ ↑k + 1 ≤ ↑n + 1
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
⊢ (↑k + 1) * π / (↑n + 1) < π

Tactic:
field_simp

Goal state after:
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
⊢ ↑k + 1 < ↑n + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case h
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
⊢ ↑(↑k + 1) * π = (↑↑n + 1) * ((↑k + 1) * π / (↑n + 1))

Tactic:
field_simp

Goal state after:
case h
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
⊢ ↑(↑k + 1) * (↑n + 1) = (↑↑n + 1) * (↑k + 1)
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
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
t : Finset ι
r : 𝕜
⊢ r ∈ s → HasDerivAt (fun y ↦ ∑ b ∈ t, f b y) (∑ i ∈ t, derivWithin (fun z ↦ f i z) s r) r

Tactic:
hr

Goal state after:
ι : 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
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
t : Finset ι
r : 𝕜
hr : r ∈ s
⊢ HasDerivAt (fun y ↦ ∑ b ∈ t, f b y) (∑ i ∈ t, derivWithin (fun z ↦ f i z) s r) r
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 : 𝕜
⊢ r ∈ s → Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r

Tactic:
hr

Goal state after:
ι : 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
⊢ Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r
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)
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
this : Irrational (cos (↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π))
⊢ (2 * ↑k + 1) * π / (2 * ↑n) = (2 * ↑k + 1) / (2 * ↑n) * π

Tactic:
field_simp

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

Goal state before:
pp: n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ ↑n * π / (2 * ↑n) = π / 2

Tactic:
field_simp

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

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
n : ℕ
⊢ (↑π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) * (1 / (↑π * x)) =
    ∏ i ∈ Finset.range n, (1 + sineTerm x i)

Tactic:
field_simp

Goal state after:
x : ℂ
h0 : x ≠ 0
n : ℕ
⊢ ∏ x_1 ∈ Finset.range n, ((↑x_1 + 1) ^ 2 - x ^ 2) / (↑x_1 + 1) ^ 2 =
    ∏ x_1 ∈ Finset.range n, ((↑x_1 + 1) ^ 2 + -x ^ 2) / (↑x_1 + 1) ^ 2
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
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.Data.Int.Fib.Basic

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

Tactic:
grind [fib_add_two, fib_two, fib_one]

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

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

Tactic:
fib_neg_natCast_add_neg_natCast,

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

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

Tactic:
apply this.comp_injective CharZero.cast_injective

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

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

Tactic:
have h1 := cot_series_rep' hz

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

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
| ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y ∧ (↑e).ker ∈ Module.End.invtSubmodule ↑y

Tactic:
simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
| e ∈ S
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
⊢ IsLimit (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
apply ShortComplex.isLimitOfIsLimitπ <;>
      apply (KernelFork.isLimitMapConeEquiv _ _).2
    · exact kernelIsKernel _
    · exact isLimit f g
    · exact kernelIsKernel _

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 0 < ↑⌊c k ^ n⌋₊

Tactic:
refine zero_lt_one.trans_le ?_

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 1 ≤ ↑⌊c k ^ n⌋₊
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊

Tactic:
refine zero_lt_one.trans_le ?_

Goal state after:
case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 ≤ ↑⌊c ^ i⌋₊
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
let q := fun X => isoWhiskerLeft _ (uliftYonedaIsoYoneda.symm.app _) ≪≫ htO.homNatIso X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful
q : (X : CostructuredArrow yoneda (colimit F)) →
  (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj X) ≅
    uliftYoneda.{max u v, v, max u v}.obj X :=
  fun X ↦
    (CostructuredArrow.toOver yoneda (colimit F)).op.isoWhiskerLeft
        (uliftYonedaIsoYoneda.symm.app ((CostructuredArrow.toOver yoneda (colimit F)).obj X)) ≪≫
      htO.homNatIso X
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Faithful

Tactic:
rw [functor]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (F C ⋙ G C ⋙ H C).Faithful
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Full

Tactic:
rw [functor]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (F C ⋙ G C ⋙ H C).Full
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits (functor C)

Tactic:
rw [functor]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits (F C ⋙ G C ⋙ H C)
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits (functor C)

Tactic:
rw [functor]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
h : (preadditiveYoneda.obj J ⋙ forget AddCommGrpCat).PreservesEpimorphisms
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (preadditiveYoneda.obj J).PreservesEpimorphisms → (yoneda.obj J).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
n : ℤ
⊢ Injective (R.cochainComplex.X n)

Tactic:
by
  by_cases hn : 0 ≤ n
  · obtain ⟨k, rfl⟩ := Int.eq_ofNat_of_zero_le hn
    exact Injective.of_iso (R.cochainComplexXIso _ _ rfl).symm inferInstance
  · exact IsZero.injective (CochainComplex.isZero_of_isStrictlyGE _ 0 _ (by lia))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ R.π'.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv

Tactic:
by
  dsimp [π']
  rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_hom_f]
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

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
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)

Tactic:
apply descHomotopy (f ≫ g)

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc (f ≫ g) K I = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc f J I ≫ desc g K J = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
X' : C
g : X' ⟶ X
⊢ (Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ = R.extMk (g ≫ f) m hm ⋯

Tactic:
have := HasDerivedCategory.standard C
  ext
  simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
    extEquivCohomologyClass_symm_mk_hom, Category.assoc]
  rw [Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_precomp, ← ShiftedHom.mk₀_comp 0 rfl,
    ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]
  simp

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

Goal state before:
pp: 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 (cokernel.π f)

Tactic:
by rwa [isoModSerre_iff_of_epi]

Goal state after: