mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

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

Tactic:
refine tendsto_cfc_fun ?tendsto ?cont

Goal state after:
case tendsto
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

case cont
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (fun x_1 ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ p⁻¹ • (cfc (fun x ↦ x ^ p) a - 1) = p⁻¹ • (a ^ p - 1)

Tactic:
rpow_eq_cfc_real ..

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
a : A
ha : a ∈ {a | IsStrictlyPositive a}
⊢ p⁻¹ • (cfc (fun x ↦ x ^ p) a - 1) = p⁻¹ • (cfc (fun x ↦ x ^ p) a - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ConcaveOn ℝ s g

Tactic:
apply isClosed_setOfPred_concaveOn.mem_of_tendsto (f := f) (b := (𝓝[>] (0 : ℝ)))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, f x ∈ {f | ConcaveOn ℝ s f}
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|

Tactic:
have hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b :=
    intervalIntegrable_inv_smul hf ha hb

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|
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) - f (b * x)) =
    (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x)

Tactic:
smul_sub

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
ε 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)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * t ^ (-1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
← rpow_add' (by grind) (by grind)

Goal state after:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ (p + -1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
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
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ

Tactic:
have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.1

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
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x / log b < log y / log b

Tactic:
div_lt_div_iff_of_pos_right (log_pos hb)

Goal state after:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x / log b < log y / log b ↔ x < y

Tactic:
div_lt_div_iff_of_pos_right (log_pos hb)

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

Goal state before:
pp: x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ 0 < deriv (fun x ↦ x * log x) x

Tactic:
have hlt : rexp (-1) < x := by simpa using hx

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

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb
    cases hb
    · simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.floor_zero, Int.log_zero_left]
    · simp_all only [Nat.cast_one, logb_one_left, Int.floor_zero, Int.log_one_left]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)

Tactic:
rintro s t ⟨hs_compact, hs_closed⟩ ht_open

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s \ t) ∧ IsClosed (s \ t)
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| < δ
⊢ ‖∫ (a : E) in K, ε.mulExpNegMulSq (g a) - ε.mulExpNegMulSq (f a) ∂P‖ ≤ δ * (P K).toReal

Tactic:
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.MulExpNegMulSqIntegral

Goal state before:
pp: case pos
ε : ℝ
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
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

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)
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
· simp only [hPP', integral_zero_measure, sub_self, abs_zero, Nat.ofNat_pos,
    mul_nonneg_iff_of_pos_left, (le_of_lt (sqrt_pos_of_pos hε))]

Goal state after:
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)
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)] <;> simp_rw [obs]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω ^ p / p)) μ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
⊢ IsCompact K → IntegrableOn f K μ

Tactic:
hK

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
hK : IsCompact K
⊢ IntegrableOn f K μ
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
⊢ ∫ (x : E), f ‖x‖ ∂μ = ∫ (x : E) in {0}ᶜ, f ‖x‖ ∂μ

Tactic:
restrict_compl_singleton

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
⊢ ∫ (x : E), f ‖x‖ ∂μ = ∫ (x : E), f ‖x‖ ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hab
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 := ⋯
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.2 - x‖ / ‖z - x‖

Tactic:
exact (le_div_iff₀ (by simpa [sub_eq_zero])).mpr ((mul_comm _ _).trans_le (hκ' p.2 hp).le)

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
θ : ℝ
h : ↑r * π = θ
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)
⊢ r • π ∈ (fun x ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}

Tactic:
have := niven_angle_eq ⟨r, h.symm⟩ hcos (by simpa using h_bnd)

Goal state after:
r : ℚ
θ : ℝ
h : ↑r * π = θ
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)
this : θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}
⊢ r • π ∈ (fun x ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by simp [le_of_lt <| Int.fract_lt_one r]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
h11,

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖(↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖‖
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 : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
⊢ K ⊆ s → IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K

Tactic:
hK

Goal state after:
α : 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 : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
⊢ IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K
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 β
⊢ K ⊆ s → IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
hK

Goal state after:
α : 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
⊢ IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg.inl
L : PeriodPair
hi₁ : 2 < 7
hi₂ : ¬Odd 2
hi₃ : ¬2 = 0
hi₄ : ¬2 = 6
⊢ ∑ x ∈ Finset.range (2 + 1),
            ↑(Nat.choose 2 x) *
                (∑ x_1 ∈ Finset.range (x + 1),
                    ↑(x.choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) * ↑(if x - x_1 = 3 then 3! else 0) -
                  if x = 0 then 2 else 0) *
              (∑ x_1 ∈ Finset.range (2 - x + 1),
                  ↑((2 - x).choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) *
                    ↑(if 2 - x - x_1 = 3 then 3! else 0) -
                if 2 - x = 0 then 2 else 0) -
          ∑ x ∈ Finset.range (2 + 1),
            (↑(Nat.choose 2 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (2 - x + 1),
                (↑((2 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ x_2 ∈ Finset.range (x + 1),
                              (↑(x.choose x_2) *
                                  if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                                ↑(if x - x_2 = 2 then 2! else 0) +
                            if x = 0 then 1 else 0) *
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            (↑((x_1 - x).choose x_2) *
                                if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                              ↑(if x_1 - x - x_2 = 2 then 2! else 0) +
                          if x_1 - x = 0 then 1 else 0)) *
                  (∑ x_2 ∈ Finset.range (2 - x - x_1 + 1),
                      (↑((2 - x - x_1).choose x_2) *
                          if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                        ↑(if 2 - x - x_1 - x_2 = 2 then 2! else 0) +
                    if 2 - x - x_1 = 0 then 1 else 0) +
        ∑ x ∈ Finset.range (2 + 1),
          (↑(Nat.choose 2 x) * if x = 0 then L.g₂ else 0) *
            (∑ x_1 ∈ Finset.range (2 - x + 1),
                (↑((2 - x).choose x_1) * if x_1 = 0 then ℘[L - 0] 0 else ↑(x_1 + 1)! * L.sumInvPow 0 (x_1 + 2)) *
                  ↑(if 2 - x - x_1 = 6 then 6! else 0) +
              ↑(if 2 - x = 4 then 4! else 0)) +
      ∑ x ∈ Finset.range (2 + 1), (↑(Nat.choose 2 x) * if x = 0 then L.g₃ else 0) * ↑(if 2 - x = 6 then 6! else 0) =
    0

Tactic:
simp [Finset.sum_range_succ]

Goal state after:
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
⊢ ∑ x ∈ Finset.range (4 + 1),
            ↑(Nat.choose 4 x) *
                (∑ x_1 ∈ Finset.range (x + 1),
                    ↑(x.choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) * ↑(if x - x_1 = 3 then 3! else 0) -
                  if x = 0 then 2 else 0) *
              (∑ x_1 ∈ Finset.range (4 - x + 1),
                  ↑((4 - x).choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) *
                    ↑(if 4 - x - x_1 = 3 then 3! else 0) -
                if 4 - x = 0 then 2 else 0) -
          ∑ x ∈ Finset.range (4 + 1),
            (↑(Nat.choose 4 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ x_2 ∈ Finset.range (x + 1),
                              (↑(x.choose x_2) *
                                  if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                                ↑(if x - x_2 = 2 then 2! else 0) +
                            if x = 0 then 1 else 0) *
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            (↑((x_1 - x).choose x_2) *
                                if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                              ↑(if x_1 - x - x_2 = 2 then 2! else 0) +
                          if x_1 - x = 0 then 1 else 0)) *
                  (∑ x_2 ∈ Finset.range (4 - x - x_1 + 1),
                      (↑((4 - x - x_1).choose x_2) *
                          if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                        ↑(if 4 - x - x_1 - x_2 = 2 then 2! else 0) +
                    if 4 - x - x_1 = 0 then 1 else 0) +
        ∑ x ∈ Finset.range (4 + 1),
          (↑(Nat.choose 4 x) * if x = 0 then L.g₂ else 0) *
            (∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) * if x_1 = 0 then ℘[L - 0] 0 else ↑(x_1 + 1)! * L.sumInvPow 0 (x_1 + 2)) *
                  ↑(if 4 - x - x_1 = 6 then 6! else 0) +
              ↑(if 4 - x = 4 then 4! else 0)) +
      ∑ x ∈ Finset.range (4 + 1), (↑(Nat.choose 4 x) * if x = 0 then L.g₃ else 0) * ↑(if 4 - x = 6 then 6! else 0) =
    0

Tactic:
· simp [Finset.sum_range_succ, show Nat.choose 4 2 = 6 by rfl, g₂]; ring

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

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

Tactic:
exact arithGeom_eq ha _

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

Goal state before:
pp: case ofNat
n : ℕ
⊢ fib (↑n + 2) = ↑(Nat.fib n) + fib (↑n + 1)

Tactic:
rw [← Nat.cast_ofNat, ← Nat.cast_add, ← Nat.cast_add_one, fib_natCast, fib_natCast,
      Nat.fib_add_two, Nat.cast_add]

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ IsNat n.minFac n

Tactic:
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
    rw [Nat.prime_def_le_sqrt]
    refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩
    exact lt_irrefl m <| calc
      m ≤ sqrt n   := hmn
      _ < k        := sqrt_lt.mpr (ble_eq_false.mp h2)
      _ ≤ n.minFac := h1.2.2
      _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn

Goal state after: