mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
hbd : HasGaussNorm v c f
t : ℕ
⊢ v ((coeff t) f) * c ^ t ≤ gaussNorm v c f

Tactic:
rw [gaussNorm_eq]
  apply le_ciSup hbd

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f g : R⟦X⟧
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
x✝ : Unit
⊢ 0 x✝ ≤ (fun x ↦ c) x✝

Tactic:
by simp [hc]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
h : p.support.Nonempty
hc : 0 ≤ c
⊢ 0 ≤ p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i

Tactic:
by
  simp only [Finset.le_sup'_iff, mem_support_iff]
  use p.natDegree
  simp_all only [support_nonempty, ne_eq, coeff_natDegree, leadingCoeff_eq_zero, not_false_eq_true,
    true_and]
  positivity

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
⊢ (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2

Tactic:
simp [← hk', Finsupp.prod_add_index' (h := (c · ^ ·)) (by grind) (by grind)]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hp : p ≠ 0
⊢ 0 < p.mahlerMeasure

Tactic:
by
  grind [exp_pos, mahlerMeasure_def_of_ne_zero]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p q : ℂ[X]
hpq : ¬p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
mul_eq_zero,

Goal state after:
case neg
p q : ℂ[X]
hpq : ¬(p = 0 ∨ q = 0)
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s : Finset ι
hs : s.Nonempty
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
⊢ g (∑ i ∈ s, f i) ≤ s.sup' hs fun x ↦ g (f x)

Tactic:
simp only [Finset.le_sup'_iff]

Goal state after:
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s : Finset ι
hs : s.Nonempty
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
⊢ ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hp : ¬p = 0
⊢ p.natDegree ∈ p.support ∧ 0 < (fun x a ↦ ‖a‖) p.natDegree (p.coeff p.natDegree)

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) = 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n

Tactic:
· ring

Goal state after:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
x : ℝ
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ ofDigits (x.digits b) = x

Tactic:
by
  simp only [ofDigits]
  rw [← Summable.hasSum_iff]
  · exact hasSum_ofDigitsTerm_digits x hb hx
  · exact summable_ofDigitsTerm

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:

Tactic:
p.supNorm = ‖p.coeff i‖ := hi
    _ ≤ (p.natDegree.choose i) * p.mahlerMeasure := p.norm_coeff_le_choose_mul_mahlerMeasure i
    _ ≤ (p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure :=
      mul_le_mul_of_nonneg_right (by exact_mod_cast Nat.choose_le_middle i p.natDegree)
        p.mahlerMeasure_nonneg

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ ↑(stdPart x) - ↑y < x

pp: case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ x < ↑(stdPart x) + ↑y

Tactic:
· apply lt_of_lt_stdPart coeRingHom h; simpa

Goal state after:
case refine_2
x : ℝ*
h : 0 ≤ ArchimedeanClass.mk x
y : ℝ
hy : 0 < y
⊢ x < ↑(stdPart x) + ↑y
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ 0 = stdPart x

Tactic:
rw [eq_comm, stdPart_eq_zero]

Goal state after:
case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ ArchimedeanClass.mk x ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)

Tactic:
rw [← cast_intCast]
  exact h.ratCast_add m

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

Goal state before:
pp: x : ℝ
p : ℤ[X]
hx : Irrational x
p_nonzero : p ≠ 0
x_is_root : (aeval x) p = 0
rid : ¬1 < p.natDegree
⊢ False

Tactic:
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩

Goal state after:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
rid : ¬1 < (C a * X + C b).natDegree
⊢ False
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ Tendsto arctan (𝓝[<] 1) (𝓝 l)

Tactic:
apply abel.congr'

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) =ᶠ[𝓝[<] 1] arctan
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y n = y.agmSequences x n

Tactic:
cases n with

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑(y - x) / ↑2 = dist x y / 2

Tactic:
NNReal.coe_two,

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑(y - x) / 2 = dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
⊢ (x.agmSequences y n).1 ≤ ⨆ n, (x.agmSequences y n).1

Tactic:
exact le_ciSup bddAbove_range_agmSequences_fst _

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

Goal state before:
pp: ⊢ artanh 0 = 0

Tactic:
by simp [artanh]

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

Goal state before:
pp: case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p

pp: case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

pp: case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p

Tactic:
· ring

Goal state after:
case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
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
x : ℝ
⊢ u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)

Tactic:
cases n with

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

Goal state before:
pp: this✝ : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x ↦ 1 - x
this : MapsTo (fun x ↦ 1 - x) (Iio 1) (Ioi 0)
⊢ 0 = 1 - 1

Tactic:
exact Eq.symm (sub_eq_zero_of_eq rfl)

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
⊢ ∀ ⦃b : ℝ⦄, b ∈ Icc 0 (1 - 1 / ↑q) → p1 < b → qaryEntropy q p1 < qaryEntropy q b

Tactic:
p2

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
⊢ p2 ∈ Icc 0 (1 - 1 / ↑q) → p1 < p2 → qaryEntropy q p1 < qaryEntropy q p2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
⊢ ∀ ⦃b : ℝ⦄, b ∈ Icc (1 - 1 / ↑q) 1 → p1 < b → qaryEntropy q b < qaryEntropy q p1

Tactic:
p2

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
⊢ p2 ∈ Icc (1 - 1 / ↑q) 1 → p1 < p2 → qaryEntropy q p2 < qaryEntropy q p1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
h1 : (1 - (↑q)⁻¹) * ↑q < p * ↑q
h2 : (1 - (↑q)⁻¹) * ↑q = ↑q - 1
⊢ ↑q - 1 < p * ↑q

Tactic:
rwa [h2] at h1

Goal state after:
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
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x) - x⁻¹ • f (b * x) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)

Tactic:
exact integral_sub (intervalIntegrable_inv_smul_comp_mul hf hε hr ha)
          (intervalIntegrable_inv_smul_comp_mul hf hε hr hb)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:

Tactic:
_ = (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

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

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ 0 < -↑(↑(n + 1))⁻¹ + -(log ↑n - log ↑(n + 1))

Tactic:
neg_sub,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ 0 < -↑(↑(n + 1))⁻¹ + (log ↑(n + 1) - log ↑n)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = deriv Gamma (1 / 2) + √π * (deriv Gamma 1 + -deriv Gamma 1)

pp: case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

pp: case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (s + 1 / 2)) (1 / 2)

Tactic:
add_neg_cancel,

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = deriv Gamma (1 / 2) + √π * 0

case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (s + 1 / 2)) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ b ^ x ≤ b ^ logb b y ↔ b ^ x ≤ y

Tactic:
rpow_logb (b_pos hb) (b_ne_one' hb) hy

Goal state after:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ b ^ x ≤ y ↔ b ^ x ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ b ^ x < b ^ logb b y ↔ b ^ x < y

Tactic:
rpow_logb (b_pos hb) (b_ne_one' hb) hy

Goal state after:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ b ^ x < y ↔ b ^ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x

Tactic:
rw [← @logb_one b]

Goal state after:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : μ (A \ K) < μ A - r
⊢ ∃ K ⊆ A, p K ∧ r < μ K

Tactic:
refine ⟨K, hK_subset, hK, ?_⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : μ (A \ K) < μ A - r
⊢ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal

Tactic:
by
  rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)), ← norm_eq_abs]
  exact norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
    (fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a : ℕ
⊢ ∃ c, c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)

Tactic:
have H : ∃ c, a < (c + 1) ^ (n + 1) := ⟨a, Nat.le_self_pow (by positivity) (a + 1)⟩

Goal state after:
n a : ℕ
H : ∃ c, a < (c + 1) ^ (n + 1)
⊢ ∃ c, c ^ (n + 1) ≤ a ∧ a < (c + 1) ^ (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (‖l‖ / 2) ^ 2 * ‖l‖ ^ 2 = ‖l‖ ^ 4 / 4

Tactic:
· ring

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

Goal state before:
pp: case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ False

Tactic:
suffices (m : ℝ) < 0 by grind

Goal state after:
case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ ↑m < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: ⊢ deriv arcsin = fun x ↦ 1 / √(1 - x ^ 2)

Tactic:
by
  funext x
  by_cases h : x ≠ -1 ∧ x ≠ 1
  · exact (hasDerivAt_arcsin h.1 h.2).deriv
  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
    simp only [not_and_or, Ne, Classical.not_not] at h
    rcases h with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
· have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn
    apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae
    simp only [hab, uIoc_of_le]
    rw [← restrict_Ioo_eq_restrict_Ioc]
    filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
    exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b, derivWithin f (Icc a b) x ∂volume = ∫ (x : ℝ) in Ioc a b, deriv f x ∂volume

Tactic:
apply MeasureTheory.integral_congr_ae

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioc a b)] deriv f
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in Ioc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
restrict_Ioc_eq_restrict_Icc

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in Icc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
have := intervalIntegrable_sqrt_one_sub_sq_inv.continuousOn_mul hf

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntervalIntegrable (fun x ↦ f x * √(1 - x ^ 2)⁻¹) volume (-1) 1
⊢ Integrable f measureT
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n m : ℤ
this :
  ∫ (x : ℝ), 2 * (eval x (T ℝ n) * eval x (T ℝ m)) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
MeasureTheory.integral_const_mul

Goal state after:
n m : ℤ
this :
  2 * ∫ (a : ℝ), eval a (T ℝ n) * eval a (T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∑ x ∈ range (2 * n), ∫ (a : ℝ), c x * eval a (↑(chebyshevTsequence ℝ) x) ∂measureT =
    ∑ x ∈ range (2 * n), c x * sumZeroes n (↑(chebyshevTsequence ℝ) x)

Tactic:
MeasureTheory.integral_const_mul

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∑ x ∈ range (2 * n), c x * ∫ (a : ℝ), eval a (↑(chebyshevTsequence ℝ) x) ∂measureT =
    ∑ x ∈ range (2 * n), c x * sumZeroes n (↑(chebyshevTsequence ℝ) x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
this :
  ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i

Tactic:
simpa [negOnePow_mul_negOnePow_mul_cancel]

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

Goal state before:
pp: case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ ((L.weierstrassPExceptSeries l₀ x i) fun x ↦ z) = (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i

Tactic:
rw [weierstrassPExceptSeries, FormalMultilinearSeries.ofScalars_apply_eq,
      FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul]

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval (cosh (arcosh x)) (T ℝ n)

Tactic:
grind [T_real_cosh, one_le_cosh]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ 1 < eval x (T ℝ n)

Tactic:
← cosh_arcosh (le_of_lt hx),

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ 1 < eval (cosh (arcosh x)) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_2
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:
exact fun t _ => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

Goal state after: