mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
this : ∀ (n : ℕ), ∃ m', f m' = v n ∧ ‖m'‖ ≤ C * ‖v n‖
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
choose u hu hnorm_u using this

Goal state after:
case neg
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
⊢ ∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case e'_5
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : ¬μ x < 1
⊢ 1 = μ x ^ 0

Tactic:
rw [rpow_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
⊢ SeminormedAddCommGroup L

Tactic:
have : NormedField L := normedField K L

Goal state after:
R : Type u_1
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
this : NormedField L
⊢ SeminormedAddCommGroup L
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: case h
R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
ginv : F' →L[R] E'
hginv : LeftInverse ⇑ginv ⇑g
⊢ LeftInverse ⇑(finv.prodMap ginv) ⇑(f.prodMap g)

Tactic:
simp [hfinv, hginv]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: case h
R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : RightInverse ⇑finv ⇑f
ginv : F' →L[R] E'
hginv : RightInverse ⇑ginv ⇑g
⊢ RightInverse ⇑(finv.prodMap ginv) ⇑(f.prodMap g)

Tactic:
simp [hfinv, hginv]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
this : ‖R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
simpa only [mul_smul, sub_smul, one_smul] using this

Goal state after:
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : RCLike 𝕜
X : Type u_4
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : Set (WeakSpace 𝕜 X)
hb : IsBounded (⇑(toWeakSpace 𝕜 X) ⁻¹' S)
hrange : closure (⇑(inclusionInDoubleDualWeak 𝕜 X) '' S) ⊆ Set.range ⇑(inclusionInDoubleDualWeak 𝕜 X)
⊢ IsCompact (closure S)

Tactic:
by
  rw [(isEmbedding_inclusionInDoubleDualWeak 𝕜 X).closure_eq_preimage_closure_image]
  apply (isEmbedding_inclusionInDoubleDualWeak 𝕜 X).isCompact_preimage' _ hrange
  exact WeakDual.isCompact_of_bounded_of_closed
    (WeakDual.isBounded_closure ((inclusionInDoubleDual 𝕜 X).lipschitz.isBounded_image hb))
    isClosed_closure

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ‖(∏ x ∈ s, (1 + f x)) * ∏ x ∈ b \ s, (1 + f x) - ∏ i ∈ s, (1 + f i)‖ < ε / 2

Tactic:
← mul_sub_one,

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
s₂ : Finset ι
hs₂ : ∀ (t : Finset ι), Disjoint t s₂ → ‖∏ i ∈ t, (1 + f i) - 1‖ < ε / (2 * r₁)
s : Finset ι := s₁ ∪ s₂
b : Finset ι
hb : s ⊆ b
⊢ ‖(∏ x ∈ s, (1 + f x)) * (∏ x ∈ b \ s, (1 + f x) - 1)‖ < ε / 2
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
h_inv : (u.restrict h_mapsto).IsInvertible
⊢ u.IsFredholm

Tactic:
obtain ⟨e, he⟩ := h_inv
  have eqL : u.domRestrict E₁ = F₁.subtypeL ∘L e := congr(F₁.subtypeL ∘L $he).symm
  have eqₗ : u.toLinearMap.domRestrict E₁ = F₁.subtype ∘ₗ e := congr(($eqL).toLinearMap)
  have h : Topology.IsStrictMap u ∧ IsClosed (u.range : Set F) := by
    rw [u.isStrictMap_isClosed_range_iff_restrict E₁ E₁_closed, eqL]
    exact ⟨F₁.isEmbedding_subtype.comp e.isHomeomorph.isEmbedding |>.isStrictMap, by simpa⟩
  have disj : Disjoint E₁ u.ker := by
    rw [disjoint_iff_comap_eq_bot, ← LinearMap.ker_domRestrict, eqₗ,
      LinearMap.ker_comp, ker_subtype, comap_bot, LinearEquiv.ker]
  refine ⟨h.1, h.2, ?_, ?_, ?_⟩
  · rw [← Submodule.fg_iff_finiteDimensional]
    exact E₁_coFG.fg_of_disjoint disj.symm
  · refine F₁_coFG.of_le (le_trans ?_ (u.range_domRestrict_le_range E₁))
    rw [eqₗ, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top, range_subtype]
  · exact .of_disjoint_of_finiteDimensional_quotient E₁_closed disj.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Goal state after:
α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
⊢ α.compProj ↑t₀ = x

Tactic:
by rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt α.compProj (f t (α.compProj t)) (Icc tmin tmax) t

Tactic:
apply hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry
    α.continuous_compProj.continuousOn (fun _ ht' ↦ α.compProj_mem_closedBall hf.mul_max_le)
    x ht |>.congr_of_mem _ ht

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ ∀ x_1 ∈ Icc tmin tmax, α.compProj x_1 = picard f (↑t₀) x α.compProj x_1
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = ((fun x ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x✝

Tactic:
rw [Function.comp_apply, comp_neg_X_leadingCoeff_eq, ← mul_rotate]

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = (-x✝) ^ (P.comp (-X)).natDegree * (-1) ^ P.natDegree * P.leadingCoeff
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
geom_sum_of_one_lt ha

Goal state after:
case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

Tactic:
by
  by_cases hp : P = 0
  · simpa [hp] using isBigO_zero Q.eval atTop
  · have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
    have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd h' h
    rcases le_iff_lt_or_eq.mp h with h | h
    · exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_atTop_zero_of_degree_lt P Q h)
    · exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_atTop_leadingCoeff_div_of_degree_eq P Q h)

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
⊢ (fun x ↦ eval x P) =O[cobounded R] fun x ↦ eval x Q

Tactic:
by_cases hQ : Q.leadingCoeff = 0

Goal state after:
case pos
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : Q.leadingCoeff = 0
⊢ (fun x ↦ eval x P) =O[cobounded R] fun x ↦ eval x Q

case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ (fun x ↦ eval x P) =O[cobounded R] fun x ↦ eval x Q
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
⊢ x ≠ i →
    v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) < v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2)

Tactic:
hneq

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) < v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ IntervalIntegrable (fun x ↦ log ‖eval (circleMap 0 1 x) p‖) MeasureTheory.volume 0 (2 * π)

Tactic:
← circleIntegrable_def fun z ↦ log ‖p.eval z‖

Goal state after:
p : ℂ[X]
⊢ CircleIntegrable (fun z ↦ log ‖eval z p‖) 0 1
Module: Mathlib.Analysis.Real.Pi.Bounds

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

Tactic:
refine lt_of_lt_of_le this (le_of_eq ?_)

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

Goal state before:
pp: x : ℝ*
r : ℝ
h : x.IsSt r
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r

Tactic:
refine ⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩

Goal state after:
case refine_1
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ 0 ≤ ArchimedeanClass.mk x

case refine_2
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ coeRingHom s ≤ x

case refine_3
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ coeRingHom s
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: y : ℝ*
r s : ℝ
hys : y.IsSt s
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
⊢ ofSeq f < y

Tactic:
rcases ofSeq_surjective y with ⟨g, rfl⟩

Goal state after:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: ⊢ ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)

Tactic:
by
    apply Antitone.tendsto_alternating_series_of_tendsto_zero
    · exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr
    · apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right
      exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
rw [dist_comm, dist_eq, ← NNReal.coe_sub (sqrt_mul_le_half_add ..), abs_eq]

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

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

Tactic:
add_div,

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

Goal state before:
pp: case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

pp: case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
· simp only [mem_singleton_iff] at hp
    simp only [hp, nnrpow_zero]
    exact concaveOn_const _ (convex_Ici _)

Goal state after:
case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
add_div,

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

Goal state before:
pp: case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn g (Ioi 0 ×ˢ s)

Tactic:
simp only [g]
    refine ContinuousOn.mul ?_ ?_
    · refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)
    · exact ContinuousOn.inv₀ (by fun_prop) (by grind)

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
have : p - 2 = p - 1 - 1 := by ring

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ 0 < ↑(↑(n + 1))⁻¹ - log ((↑(n + 1) + 1) / (↑n + 1))

Tactic:
add_div,

Goal state after:
n : ℕ
⊢ 0 < ↑(↑(n + 1))⁻¹ - log (↑(n + 1) / (↑n + 1) + 1 / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf

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

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

Tactic:
mul_inv_cancel₀
      this,

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = x ^ p * 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹

Tactic:
add_div,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
s x : ℝ
| rexp (-a * x ^ 2)

Tactic:
← sq_abs

Goal state after:
a : ℝ
ha : 0 < a
s x : ℝ
| rexp (-a * |x| ^ 2)
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 : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Nat.cast_le]

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x = |x|

Tactic:
by
  apply log_injOn_pos
  · simp only [Set.mem_Ioi]
    apply rpow_pos_of_pos b_pos
  · simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]
  rw [log_rpow b_pos, logb, log_abs]
  field [log_ne_zero_of_pos_of_ne_one b_pos b_ne_one]

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

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

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

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

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

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

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

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

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]
  exact log_lt_log hx hxy

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 0 ≤ 2 * y

Tactic:
simp [hynonneg]

Goal state after:
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) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)

Tactic:
let f : ℝ → ℝ := (Set.Ici (n - 1 : ℝ)).piecewise (descPochhammer ℝ n).eval 0

Goal state after:
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)
f : ℝ → ℝ := (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)