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

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log (cexp (z * I) / (cos (-z) + sin (-z) * I)) = z

Tactic:
← exp_mul_I,

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log (cexp (z * I) / cexp (-z * I)) = z
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b

Tactic:
CFC.sqrt_eq_nnrpow a,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ a ^ (1 / 2) ≤ sqrt b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
⊢ Monotone fun a ↦ a ^ ↑q

Tactic:
rw [hq]
    intro a b hab
    by_cases ha : 0 ≤ a
    · have hb : 0 ≤ b := ha.trans hab
      simp [CFC.rpow_zero a, CFC.rpow_zero b]
    · have : a ^ (0 : ℝ) = 0 := cfc_apply_of_not_predicate a ha
      simp [this]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Tendsto (fun p a ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0) (𝓝[>] 0)
    (𝓝 fun a ↦ if a ∈ {b | IsStrictlyPositive b} then log a else 0)

Tactic:
rw [tendsto_pi_nhds]
  intro a
  by_cases ha : IsStrictlyPositive a
  · simpa [ha] using CFC.tendsto_cfc_rpow_sub_one_log ha
  · simp_all

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

Tactic:
exact zpos.spectrum_pos hr

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 : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ

Tactic:
filter_upwards [eventually_atTop.2 ⟨max 1 (N / min a b), fun r hr ↦ hr⟩] with t ht

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
⊢ ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t⁻¹ - (t + x)⁻¹

Tactic:
sub_nonneg

Goal state after:
case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ (t + x)⁻¹ ≤ t⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
have hici : Ici (0 : A) = addl ⁻¹' addl '' Ici 0 := by
    rw [Set.preimage_image_eq _ haddl]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0)

Tactic:
by
  refine ContinuousOn.congr ?_ <| rpowIntegrand₀₁_eqOn_pow_div hp hx
  have h₀ : ContinuousOn (· ^ (p - 1) : ℝ → ℝ) (Ioi 0) := .rpow_const (by fun_prop) <|
    fun t ht => .inl ht.ne'
  fun_prop (disch := grind -abstractProof)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑π

Tactic:
Gammaℂ_def,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ 2 * (2 * ↑π) ^ (-(s + 1)) * Gamma (s + 1) = s.Gammaℂ * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ 2 * (2 * ↑π) ^ (-(s + 1)) * Gamma (s + 1) = s.Gammaℂ * s / 2 / ↑π

Tactic:
Gammaℂ_def,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ 2 * (2 * ↑π) ^ (-(s + 1)) * Gamma (s + 1) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < (s / 2).re

Tactic:
div_ofNat_re

Goal state after:
case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Gammaℂ 1 = 1 / ↑π

Tactic:
Gammaℂ_def,

Goal state after:
⊢ 2 * (2 * ↑π) ^ (-1) * Gamma 1 = 1 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
Gammaℂ_def,

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
    · exact tendsto_id.const_mul_atTop hx
    · simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x
    · simpa [Set.image_mul_left_Ioi hx] using continuousOn_rpowIntegrand₀₁ hp hx.le
    · simpa [Set.image_mul_left_Ici hx] using integrableOn_rpowIntegrand₀₁_Ici hp hx.le
    · simp only [Function.comp]
      rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
      exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _

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

Goal state before:
pp: p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2)

Tactic:
rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith) zero_lt_one]

Goal state after:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = 1 / 2 * (-1 ^ (p - 2 + 1) / (p - 2 + 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi]

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
⊢ ∀ a ∈ Ioi 0, (↑p).rpowIntegrand₀₁ a 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
k : ℕ
⊢ logb b (x ^ k) = ↑k * logb b x

Tactic:
by
  rw [logb, logb, log_pow, mul_div_assoc]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(Nat.clog b ⌈↑(n + 1)⌉₊) = ↑(Nat.clog b (n + 1))

pp: case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(n + 1)

Tactic:
(Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr

Goal state after:
case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(Nat.clog b n.succ) = ↑(Nat.clog b (n + 1))

case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(n.succ - 1) < ↑(n + 1) ∧ ↑(n + 1) ≤ ↑n.succ

case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0

Tactic:
simp only [Right.neg_neg_iff, Set.mem_Iio]
    apply rpow_pos_of_pos b_pos

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ x * log x) (Ici (rexp (-1)))

Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) continuous_mul_log.continuousOn fun x hx ↦ ?_

Goal state after:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ 0 < deriv (fun x ↦ x * log x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |x| < logb b |y|

Tactic:
refine logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
⊢ (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) A → ∀ r < μ A, ∃ K ⊆ A, IsCompact K ∧ r < μ K

Tactic:
⟨hA1, hA2⟩

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
⊢ ∀ r < μ A, ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ Differentiable 𝕜 fun x ↦ Polynomial.eval x (descPochhammer 𝕜 n)

Tactic:
simp [descPochhammer_eval_eq_prod_range, Differentiable.fun_finsetProd]

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

Goal state before:
pp: ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| < √ε

Tactic:
exact (abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
      f (IsClosed.measurableSet hKcl) hε hKP'bound)

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

Goal state before:
pp: case succ
n a : ℕ
H : ∃ c, a < (c + 1) ^ (n + 1)
k : ℕ
hc : k + 1 = Nat.find H
⊢ (k + 1) ^ (n + 1) ≤ a

Tactic:
simpa using Nat.find_min H hc.le

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

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
⊢ TendstoLocallyUniformlyOn
    (deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) ℘'[L - l₀]
    atTop (↑L.lattice \ {l₀})ᶜ

Tactic:
refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
⊢ ∀ (n : Finset ↥L.lattice),
    Set.EqOn (fun x2 ↦ ∑ i ∈ n, (fun l z ↦ if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) i x2)
      ((deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) n)
      (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (c : ↥L.lattice), if ↑((Equiv.addRight l) c) = l₀ then 0 else -2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3

Tactic:
simp only [Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub, eq_sub_iff_add_eq]

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

Goal state before:
pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
simp only [Set.mem_compl_iff, Set.mem_sdiff, SetLike.mem_coe, Set.mem_singleton_iff, not_and,
        Decidable.not_not, eq_sub_iff_add_eq] at hx ⊢
      exact fun H ↦ hx (by simpa using sub_mem H l.2)

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
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ (μ.toSphere.real univ •
      ∫ (x : ↑(Ioi 0)), f ↑x ∂(Measure.comap Subtype.val volume).withDensity fun r ↦ ↑(↑r ^ (dim E - 1)).toNNReal) =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
integral_withDensity_eq_integral_smul,

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ μ.toSphere.real univ • ∫ (x : ↑(Ioi 0)), (↑x ^ (dim E - 1)).toNNReal • f ↑x ∂Measure.comap Subtype.val volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

case f_meas
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
line2 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| ≤ √ε
line6 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| ≤ √ε
line4 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'| = 0
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
calc
      |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x, mulExpNegMulSq ε (f x) ∂P'|
    ≤ |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P|
      + |∫ x in K, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (g x) ∂P|
      + |∫ x in K, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P|
      + |∫ x, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P'|
      + |∫ x, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (g x) ∂P'|
      + |∫ x in K, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (f x) ∂P'|
      + |∫ x in K, mulExpNegMulSq ε (f x) ∂P' - ∫ x, mulExpNegMulSq ε (f x) ∂P'| :=
        @dist_triangle8 ℝ _ _ _ _ _ _ _ _ _
  _ ≤ 6 * √ε := by linarith

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

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (∏ x ∈ Finset.range i, -1) * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
Finset.prod_const,

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ (Finset.range i).card * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2

Tactic:
rw [hz, ← Complex.exp_nat_mul]

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑2 * (↑k / (2 * ↑n) * ↑π * I))
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
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ 0 = sumZeroes n (T ℝ ↑i)

Tactic:
sumZeroes_T_of_not_dvd this

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ 0 = 0
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
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ (-1) ^ i * (-1) ^ i

Tactic:
← neg_pow',

Goal state after:
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
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ (- -1) ^ i