mathlib-initiative/mathlib-tactics huggingface dataset:
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‖
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₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 2‖ * ((‖↑p.2 - x‖ ^ 3)⁻¹ / ‖↑p.2 - x‖ ^ p.1) * ‖z - x‖ ^ (p.1 + 1) =
    ‖↑p.1 + 2‖ * (‖z - x‖ ^ p.1 / ‖↑p.2 - x‖ ^ p.1) * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
;

Goal state after:
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₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 2‖ * ((‖↑p.2 - x‖ ^ 3)⁻¹ / ‖↑p.2 - x‖ ^ p.1) * ‖z - x‖ ^ (p.1 + 1) =
    ‖↑p.1 + 2‖ * (‖z - x‖ ^ p.1 / ‖↑p.2 - x‖ ^ p.1) * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)
Module: Mathlib.NumberTheory.Niven

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

Tactic:
;

Goal state after:
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ∈ Set.Icc (0 * π) (1 * π)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(r - ↑⌊r⌋) * π) = ↑((-1) ^ ⌊r⌋ * q)

Tactic:
;

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(r - ↑⌊r⌋) * π) = ↑((-1) ^ ⌊r⌋ * q)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos ((↑r - ↑⌊r⌋) * π) = (-1) ^ ⌊r⌋ * ↑q

Tactic:
;

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos ((↑r - ↑⌊r⌋) * π) = (-1) ^ ⌊r⌋ * ↑q
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
;

Goal state after:
case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
r : ℚ
hr : 3 < Rat.den 0
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
;

Goal state after:
case inl
r : ℚ
hr : 3 < Rat.den 0
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
;

Goal state after:
case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inl
r : ℚ
hr : 3 < (1 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
;

Goal state after:
case inr.inl
r : ℚ
hr : 3 < (1 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
;

Goal state after:
case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
r : ℚ
hr : 3 < (1 / 2).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
;

Goal state after:
case inr.inr.inl
r : ℚ
hr : 3 < (1 / 2).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False

Tactic:
;

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (2 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False

Tactic:
;

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (2 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: case h
x : ℤ × ℤ
⊢ (fun n ↦ x ∈ box n) (max x.1.natAbs x.2.natAbs) ∧ ∀ (y : ℕ), (fun n ↦ x ∈ box n) y → y = max x.1.natAbs x.2.natAbs

Tactic:
;

Goal state after:
case h
x : ℤ × ℤ
⊢ (fun n ↦ x ∈ box n) (max x.1.natAbs x.2.natAbs) ∧ ∀ (y : ℕ), (fun n ↦ x ∈ box n) y → y = max x.1.natAbs x.2.natAbs
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case h
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ 1 < 2

Tactic:
;

Goal state after:
case h
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ 1 < 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)

Tactic:
;

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
;

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ n < n + 1

Tactic:
;

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ n < n + 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (↑n✝ + 1 + 1) * L.sumInvPow l (n✝ + 1 + 2) =
    (↑n✝ + 1 + 1) * ((↑n✝ + 1) * ↑n✝!) * L.sumInvPow l (n✝ + 1 + 2) / ((↑n✝ + 1) * ↑n✝!)

Tactic:
;

Goal state after:
case succ
L : PeriodPair
l : ℂ
n✝ : ℕ
⊢ (↑n✝ + 1 + 1) * L.sumInvPow l (n✝ + 1 + 2) =
    (↑n✝ + 1 + 1) * ((↑n✝ + 1) * ↑n✝!) * L.sumInvPow l (n✝ + 1 + 2) / ((↑n✝ + 1) * ↑n✝!)
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 ≤ ↑n * (arccos x / π)

Tactic:
;

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

Goal state before:
pp: L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l

Tactic:
by
  simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    L.coeff_weierstrassPExceptSeries,
    ← L.weierstrassPExceptSummand_of_notMem _ L.ω₁_div_two_notMem_lattice]

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

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x ↑r

Tactic:
by
  simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
  exact L.hasFPowerSeriesOnBall_weierstrassPExcept _ x r hr0
    (hr.trans (Set.compl_subset_compl.mpr Set.sdiff_subset))

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0

Tactic:
;

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ ↑n < ↑k

Tactic:
;

Goal state after:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ ↑n < ↑k
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x✝ : ℕ
⊢ L.sumInvPow 0 x✝ = L.G x✝

Tactic:
;

Goal state after:
L : PeriodPair
x✝ : ℕ
⊢ L.sumInvPow 0 x✝ = L.G x✝
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i ↦ ‖![(↑i).1, (↑i).2]‖ ^ (-k)) ∧
    Summable fun j ↦ ∑' (i : ↑↑(box j)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

Tactic:
refine ⟨fun n ↦ (hasSum_fintype (β := box (α := ℤ × ℤ) n) _).summable, ?_⟩

Goal state after:
k : ℝ
hk : 2 < k
⊢ Summable fun j ↦ ∑' (i : ↑↑(box j)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ 0 = 2 ^ 2 - 4

Tactic:
;

Goal state after:
case pos
L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : z = 0
⊢ 0 = 2 ^ 2 - 4
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
⊢ ∀ y ∈ s, Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s y

Tactic:
intro r

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 : 𝕜
⊢ r ∈ s → Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ -(2 * (4 * (↑3! * L.G 4) * ↑3!)) + -(4 * (↑3! * L.G 4) * ↑3! * 2) -
        4 * (6 * (↑3! * L.G 4) * 2 + (6 * (↑3! * L.G 4) * 2 + 6 * (↑3! * L.G 4) * 2)) +
      60 * L.G 4 * ↑4! =
    0

Tactic:
;

Goal state after:
case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ -(2 * (4 * (↑3! * L.G 4) * ↑3!)) + -(4 * (↑3! * L.G 4) * ↑3! * 2) -
        4 * (6 * (↑3! * L.G 4) * 2 + (6 * (↑3! * L.G 4) * 2 + 6 * (↑3! * L.G 4) * 2)) +
      60 * L.G 4 * ↑4! =
    0
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:
;

Goal state after:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z : ℂ
w : ↥L.lattice
⊢ L.relation (z + ↑w) = L.relation z
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ.e_a
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k

Tactic:
add_comm _ n,

Goal state after:
case succ.e_a
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (n + 1), a ^ k
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

Tactic:
;

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ a * arithGeom a b u₀ n + b = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
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)) * π))
⊢ Irrational (cos ((2 * ↑k + 1) * π / (2 * ↑n)))

Tactic:
;

Goal state after:
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)) * π))
⊢ Irrational (cos ((2 * ↑k + 1) * π / (2 * ↑n)))
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) = ↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π

Tactic:
;

Goal state after:
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) = ↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π
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:
;

Goal state after:
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) * π
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).natAbs / (2 * ↑n).gcd (2 * ↑k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
;

Goal state after:
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).natAbs / (2 * ↑n).gcd (2 * ↑k + 1)) = 2 * n / (2 * n).gcd (2 * k + 1)
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:
;

Goal state after:
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)
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))
⊢ cos (↑n * π / ↑(2 * n)) = 0

Tactic:
;

Goal state after:
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))
⊢ cos (↑n * π / ↑(2 * n)) = 0
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:
;

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

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
;

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.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 : (f.sum fun mi r ↦ r • mi) = (⇑derivative)^[k] (T ℝ ↑n)
⊢ ∑ p ∈ f.support, f p • p = f.sum fun mi r ↦ r • mi

Tactic:
;

Goal state after:
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 : (f.sum fun mi r ↦ r • mi) = (⇑derivative)^[k] (T ℝ ↑n)
⊢ ∑ p ∈ f.support, f p • p = f.sum fun mi r ↦ r • mi
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
n : ℤ
m : ℕ
⊢ fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + (fib (↑(m + 1) - 1) * fib n + fib ↑(m + 1) * fib (n + 1)) =
    fib (↑m - 1) * fib n + fib ↑m * fib (n + 1) + fib ↑m * fib n + fib (↑m + 1) * fib (n + 1)