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

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) =
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)

Tactic:
agmSequences,

Goal state after:
x y : ℝ≥0
n : ℕ
⊢ (fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ (fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    (sqrt ((x.agmSequences y n).1 * (x.agmSequences y n).2), ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)

Tactic:
agmSequences,

Goal state after:
x y : ℝ≥0
n : ℕ
⊢ (fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    (sqrt
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
key : Tendsto (fun n_1 ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2

Tactic:
agmSequences,

Goal state after:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun n_1 ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1]
        (((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1,
          ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2)).2 =
    ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
suffices -p * log p < (1 - p) * log (1 - p) by linarith

Goal state after:
p : ℝ
hp : p < 0
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
rw [← binEntropy_one_sub]; exact binEntropy_neg_of_neg (sub_neg.2 hp)

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

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))

Goal state after:
case hf
⊢ Tendsto (fun x ↦ log (1 - x)) (𝓝[<] 1) atBot

case hg
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (1 - 2⁻¹)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) + 2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂' x * v₂ x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have (x : _) : u₂' x = (2 * n + 1) * f x ^ n - 2 * n * f x ^ (n - 1) := by
    cases n with
    | zero => simp [u₂']
    | succ n => ring!

Goal state after:
case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) + 2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂' x * v₂ x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
⊢ -(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) * θ + 2 * (↑0 + 1) * (2 * ↑0 + 1) * I 0 θ * θ -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ

Tactic:
mul_assoc _ (I 0 θ),

Goal state after:
θ : ℝ
⊢ -(2 * 2 * ((↑0 + 1) * (0 ^ 0 * cos θ))) * θ + 2 * (↑0 + 1) * (2 * ↑0 + 1) * (I 0 θ * θ) -
      4 * (↑0 + 1) * ↑0 * I (0 - 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
hb' : b = 1
⊢ 0 < a + b * r

Tactic:
simp only [ha', hb', one_mul, zero_add, gt_iff_lt]

Goal state after:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
hb' : b = 1
⊢ 0 < r
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
h_ev :
  (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x
⊢ Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (𝓝[>] 0 ×ˢ atTop) (𝓝 (log (b / a) • (L - R)))

Tactic:
tendsto_congr' h_ev,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
h_ev :
  (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x
⊢ Tendsto (fun p ↦ (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x) (𝓝[>] 0 ×ˢ atTop)
    (𝓝 (log (b / a) • (L - R)))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
by_cases ht' : t = 0
  case neg =>
    have hxt : t + x ≠ 0 := by positivity
    calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm
  case pos =>
    push _ ∈ _ at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
have h_diff {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ Gamma s :=
    differentiableAt_Gamma fun m ↦ ((neg_nonpos.mpr m.cast_nonneg).trans_lt hs).ne'
  have h_diff' {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s :=
    .comp (g := Gamma) _ (h_diff <| mul_pos two_pos hs) (differentiableAt_id.const_mul _)
  refine (h_diff one_half_pos).hasDerivAt.congr_deriv ?_
  -- We calculate the deriv of Gamma at 1/2 using the doubling formula, since we already know
  -- the derivative of Gamma at 1.
  calc deriv Gamma (1 / 2)
  _ = (deriv (fun s ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2)) + √π * γ := by
    rw [deriv_fun_mul, Gamma_one_half_eq,
      add_assoc, ← mul_add, deriv_comp_add_const,
      (by norm_num : 1 / 2 + 1 / 2 = (1 : ℝ)), Gamma_one, mul_one,
      eulerMascheroniConstant_eq_neg_deriv, add_neg_cancel, mul_zero, add_zero]
    · apply h_diff; simp -- s = 1
    · exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt -- s = 1
  _ = (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2)) + √π * γ := by
    rw [funext Gamma_mul_Gamma_add_half]
  _ = √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]
    apply DifferentiableAt.mul
    · exact .comp (g := Gamma) _ (by apply h_diff; simp) -- s = 1
        (differentiableAt_id.const_mul _)
    · exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero
  _ = √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) +
              deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [deriv_fun_mul]
    · simp
    · exact h_diff' one_half_pos
    · exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero
  _ = √π * (-2 * γ + deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    congr 3
    change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _
    rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
    · rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
    · apply h_diff; simp -- s = 1
    · fun_prop
  _ = √π * (-2 * γ + -(2 * log 2) + γ) := by
    congr 3
    apply HasDerivAt.deriv
    have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
    · simpa
    simp_rw [mul_comm (2 : ℝ) _]
    apply HasDerivAt.const_sub
    exact hasDerivAt_mul_const (2 : ℝ)
  _ = -√π * (γ + 2 * log 2) := by ring

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-(↑(Nat.clog b ⌈r⁻¹⌉₊) - 1))

Tactic:
← Int.ofNat_one,

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-(↑(Nat.clog b ⌈r⁻¹⌉₊) - ↑1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
hg : ContinuousOn (fun z ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (fun z ↦ 1 + z) (spectrum ℝ x)
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
← NNReal.coe_le_coe,

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ↑‖deriv ε.mulExpNegMulSq x‖₊ ≤ ↑1
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤ ∑ i ∈ t, w i * ↑((p i).choose n)

Tactic:
by
  simp_rw [Nat.cast_choose_eq_descPochhammer_div,
    mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]
  apply div_le_div_of_nonneg_right _ (by positivity)
  exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ ENNReal.ofReal (↑r ^ dim E) * μ (Ioo 0 1 • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ dim E / (↑(dim E - 1) + 1))

Tactic:
Nat.cast_pred hpos,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ ENNReal.ofReal (↑r ^ dim E) * μ (Ioo 0 1 • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ dim E / (↑(dim E) - 1 + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

Tactic:
simp only [zero_add, add_zero, *]

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2 + 0 = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

Tactic:
simp only [zero_add, add_zero, *]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this✝ : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
hdim : dim E ≠ 0
this : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

Tactic:
simp (disch := positivity) [μ.addHaar_ball_of_pos (r := ε / 4), ENNReal.ofReal_div_of_pos,
      toSphereBallBound, mul_assoc, ENNReal.ofNNReal_toNNReal, this, hdim, hε]

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ z ∈ (↑L.lattice \ {0 - ↑l})ᶜ

Tactic:
by simp [hz]

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ Integrable f measureT

Tactic:
replace hf : ContinuousOn f (Set.uIcc (-1) 1) := by rwa [Set.uIcc_of_lt (by norm_num)]
  have := intervalIntegrable_sqrt_one_sub_sq_inv.continuousOn_mul hf
  rw [intervalIntegrable_iff, Set.uIoc_of_le (by norm_num)] at this
  rw [measureT, restrict_withDensity (by measurability),
    integrable_withDensity_iff (by fun_prop) (by simp)]
  unfold IntegrableOn at this
  convert! this

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

Goal state before:
pp: a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
have hπ : π / 2 = a ^ 2 / 2 :=
    tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)

Goal state after:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = a ^ 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 √π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (θ : ℝ) in 0..π, cos (↑n * θ) = 0

Tactic:
integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn),

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ (↑n)⁻¹ • ∫ (x : ℝ) in ↑n * 0..↑n * π, cos x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)

Tactic:
by
    rw [Complex.exp_neg] at this
    have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
    apply hf this (Complex.exp_ne_zero _) (by grind [exp_sub_one_ne_zero])

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * sin (↑q * ↑π))

Tactic:
rw [sin.eq_1, mul_div_cancel₀ _ two_ne_zero]
  exact (isIntegral_exp_neg_rat_mul_pi_mul_I q).sub (isIntegral_exp_rat_mul_pi_mul_I q)
    |>.mul isIntegral_int_I

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (iterateDerivativeC n k x) P = eval x ((⇑derivative)^[k] P)

Tactic:
by
  simp_rw [sumNodes, iterateDerivativeC]
  have h₁ : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]; grw [hP]; norm_cast; simp
  convert!
    (Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_node n).injOn h₁
        (show k < _ by simp [hk]) x).symm
  rw [Finset.mul_sum]
  grind [Nat.range_succ_eq_Iic, Nat.card_Iic]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
u : α → ℝ
hu1 : Summable u
hu2 : ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
filter_upwards using hu2

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

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) ↑(Finset.range n)

Tactic:
exact (Finset.range n).nodup_map_iff_injOn.mp (roots_U_real_nodup n)

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≤ n
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (cos (↑k * π / ↑n))

Tactic:
by
  cases k.even_or_odd
  case inl hk₂ => exact .inr (isMaxOn_T_real hn hk hk₂)
  case inr hk₂ => exact .inl (isMinOn_T_real hn hk hk₂)

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

Goal state before:
pp: Z : Set ℂ
hZ : IsCompact Z
⊢ ∃ u, Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j

Tactic:
have hf : ContinuousOn (fun x : ℂ => ‖-x ^ 2‖) Z := by
    fun_prop
  obtain ⟨s, hs⟩ := bddAbove_def.mp (IsCompact.bddAbove_image hZ hf)
  refine ⟨fun n : ℕ => ‖(s : ℂ) / (n + 1) ^ 2‖, ?_, ?_⟩
  · simpa using summable_pow_div_add (s : ℂ) 2 1 (Nat.one_lt_two)
  · simp only [norm_neg, norm_pow, Set.mem_image, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, sineTerm, norm_div, norm_real, norm_eq_abs] at *
    intro n x hx
    gcongr
    apply le_trans (hs x hx) (le_abs_self s)

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

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
⊢ z ∈ ℍₒ

Tactic:
by simp [hz]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ unop (Subobject.underlying.obj R) :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
q₂ : unop (Subobject.underlying.obj R) ⟶ ∏ᶜ fun P ↦ unop (Subobject.underlying.obj P) :=
  section_ (Pi.π (fun P ↦ unop (Subobject.underlying.obj P)) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ factorThruImage (h ≫ f) = 0

Tactic:
exact zero_of_comp_mono q
    (by rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero])

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f 0).fst

pp: case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨0, ?base.refine_1⟩ = { obj := f x, property := ⋯ }.obj

Tactic:
· simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
        exact ULift.up x

Goal state after:
case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨0, id { down := x }⟩ = { obj := f x, property := ⋯ }.obj
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := f x, property := ⋯ }.obj

Tactic:
| base x =>

Goal state after: