mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hD : 0 ≤ D
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (i : ι), ‖f i‖ ≤ D
s : Finset ι
⊢ ∀ (i : ι), ‖(B i).flip‖ ≤ K

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A)

Tactic:
suffices IsStrictMap (uₛ.prodMap uₐ) ↔ IsStrictMap uₐ by
    rwa [u_restr_eq, u_eq, ← (isEmbedding_subtypeL _).isStrictMap_iff,
      ← Ψ.isHomeomorph.isEmbedding.isStrictMap_iff,
      ← Φ.symm.isHomeomorph.isQuotientMap.isStrictMap_iff]

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑uₐ
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₁
e : ↥E₁ ≃L[𝕜] ↥F₁
he : ↑e = u.restrict h_mapsto
eqL : u.domRestrict E₁ = F₁.subtypeL ∘SL ↑e
eqₗ : (↑u).domRestrict E₁ = F₁.subtype ∘ₗ ↑↑e
⊢ IsClosed[inst✝⁵] ↑(↑(F₁.subtypeL ∘SL ↑e)).range

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
u v : E →L[𝕜] F
A : Submodule 𝕜 E
inst✝ : A.CoFG
h_eqOn : EqOn ⇑u ⇑v ↑A
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝⁴] ↑(↑u).range ↔ IsStrictMap ⇑v ∧ IsClosed[inst✝⁴] ↑(↑v).range

Tactic:
replace h_eqOn : EqOn u v A.topologicalClosure := h_eqOn.closure (by fun_prop) (by fun_prop)
  simp_rw [u.isStrictMap_isClosed_range_iff_restrict _ A.isClosed_topologicalClosure,
    v.isStrictMap_isClosed_range_iff_restrict _ A.isClosed_topologicalClosure,
    LinearMap.coe_range, ContinuousLinearMap.coe_coe, ContinuousLinearMap.coe_domRestrict,
    domRestrict_eq_domRestrict_iff.mpr h_eqOn]

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

Goal state before:
pp: case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
⊢ x ∈ ↑(lowerClosure s)

Tactic:
obtain ⟨a, ha⟩ := hx.bddBelow_range

Goal state after:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
hs : IsClosed s
hs' : BddAbove s
val✝ : Fintype ι
f : ℕ → ι → ℝ
x : ι → ℝ
hx : Filter.Tendsto f Filter.atTop (nhds x)
g : ℕ → ι → ℝ
hg : ∀ (n : ℕ), g n ∈ s
hfg : ∀ (n : ℕ), f n ≤ g n
this : BoundedGENhdsClass ℝ
a : ι → ℝ
ha : a ∈ lowerBounds (range f)
⊢ x ∈ ↑(lowerClosure s)
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = ↑y ∘SL adjoint x ∘SL ↑y.symm
x : V →L[𝕜] V
⊢ adjoint ↑y ∘SL ↑y ∘SL adjoint x ∘SL ↑y.symm = adjoint x ∘SL adjoint ↑y

Tactic:
← this x,

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = ↑y ∘SL adjoint x ∘SL ↑y.symm
x : V →L[𝕜] V
⊢ adjoint ↑y ∘SL (adjoint ↑y.symm ∘SL adjoint x) ∘SL adjoint ↑y = adjoint x ∘SL adjoint ↑y
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace 𝕜 V
inst✝⁷ : CompleteSpace V
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : InnerProductSpace 𝕜 W
inst✝⁴ : CompleteSpace W
F : Type u_4
inst✝³ : EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝² : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst✝¹ : StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝ : ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
U : V ≃ₗᵢ[𝕜] W
hU : ↑f = U.conjStarAlgEquiv
this : ∀ (a : V →L[𝕜] V), f a = U.conjStarAlgEquiv a
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
le_def,

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace 𝕜 V
inst✝⁷ : CompleteSpace V
inst✝⁶ : NormedAddCommGroup W
inst✝⁵ : InnerProductSpace 𝕜 W
inst✝⁴ : CompleteSpace W
F : Type u_4
inst✝³ : EquivLike F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝² : NonUnitalAlgEquivClass F 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
inst✝¹ : StarHomClass F (V →L[𝕜] V) (W →L[𝕜] W)
inst✝ : ContinuousMapClass F (V →L[𝕜] V) (W →L[𝕜] W)
f : F
x y : V →L[𝕜] V
U : V ≃ₗᵢ[𝕜] W
hU : ↑f = U.conjStarAlgEquiv
this : ∀ (a : V →L[𝕜] V), f a = U.conjStarAlgEquiv a
⊢ (f y - f x).IsPositive ↔ (y - x).IsPositive
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: n : ℕ
θ : AddCircle (2 * π)
⊢ (toAddCircle (X ^ n)) θ = (fourier ↑n) θ

Tactic:
simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:
pp: n : ℕ
c : ℂ
θ : AddCircle (2 * π)
⊢ (toAddCircle ((monomial n) c)) θ = (c • fourier ↑n) θ

Tactic:
simp [toAddCircle, AddCircle.toCircle_nsmul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
n : ℕ
⊢ dist α ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)

Tactic:
← iterate_zero_apply (next hf hx) α

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist α ((next hf hx)^[m]^[n] α) ≤
    ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range n, ↑C ^ i) *
      dist α (next hf hx α)

Tactic:
← iterate_zero_apply (next hf hx) α

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ 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
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range n, ↑C ^ i) *
      dist α (next hf hx α)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax = tmin
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmin)

Tactic:
Icc_self

Goal state after:
case neg.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax = tmin
⊢ ContDiffOn ℝ (↑n) α {tmin}
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ p.mahlerMeasure ≤ rexp (circleAverage (fun x ↦ log (p.sum fun x a ↦ ‖a‖)) 0 1)

Tactic:
mahlerMeasure_def_of_ne_zero hp,

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp (circleAverage (fun x ↦ log (p.sum fun x a ↦ ‖a‖)) 0 1)
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 ^ (n * 3 + 2) = 2 ^ (n + 2 + 2 * n)

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

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

Tactic:
· rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]

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

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

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ (ofDigits fun x ↦ Fin.last b) = 1

Tactic:
simp only [ofDigits, ofDigitsTerm, ← inv_pow]

Goal state after:
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ∑' (n : ℕ), ↑↑(Fin.last b) * (↑(b + 1))⁻¹ ^ (n + 1) = 1
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ ↑a / ↑b ≤ √(2 + ↑c / ↑d)

Tactic:
apply le_sqrt_of_sq_le

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ π + 1 / 2 < ↑3 + 1

Tactic:
grw [pi_lt_d2]

Goal state after:
⊢ 3.15 + 1 / 2 ≤ ↑3 + 1
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ (↑b - 1) * (↑b ^ (n + 1))⁻¹ ≤ (↑b ^ n)⁻¹

Tactic:
calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind

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

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

Tactic:
· apply lt_of_stdPart_lt coeRingHom h; simpa

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

Goal state before:
pp: x : ℝ
hx : Irrational x
b : ℤ
p_nonzero : C 0 * X + C b ≠ 0
x_is_root : (aeval x) (C 0 * X + C b) = 0
this : ↑0 * x = -↑b
⊢ b = 0

Tactic:
by simpa

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + 0

Tactic:
by simpa

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 < x + 0

Tactic:
by simpa

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

Goal state before:
pp: ⊢ StrictMonoOn (fun x ↦ x + √(x ^ 2 - 1)) (Ioi 0)

Tactic:
exact strictMonoOn_id.add_monotone fun x (hx : 0 < x) y (hy : 0 < y) hxy ↦ by gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ ‖z * I‖ < 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
⊢ ‖-(z * I)‖ < 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
⊢ ‖z * I‖ < 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ ‖-(z * I)‖ < 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
hx : ‖x‖ < 1
⊢ ‖↑x‖ < 1

Tactic:
by simpa

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

Goal state before:
pp: ⊢ binEntropy 0 = 0

Tactic:
simp [binEntropy]

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

Goal state before:
pp: ⊢ binEntropy 1 = 0

Tactic:
simp [binEntropy]

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

Goal state before:
pp: k : ℕ
| fun n ↦ ↑(n.choose k)

Tactic:
intro n
    rw [choose_eq_descFactorial_div_factorial,
      cast_div (n.factorial_dvd_descFactorial k) (mod_cast k.factorial_ne_zero)]

Goal state after:
k n : ℕ
| ↑(n.descFactorial k) / ↑k !
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0

Tactic:
obtain hp₁ | hp₁ := h.2.lt_or_gt.symm

Goal state after:
case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc 0 (1 - 1 / ↑q))

Tactic:
exact qaryEntropy_continuous.continuousOn

Goal state after:
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
⊢ ContinuousOn (qaryEntropy q) (Icc (1 - 1 / ↑q) 1)

Tactic:
exact qaryEntropy_continuous.continuousOn

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

pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ 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:
case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : 0 < q
⊢ Monotone fun a ↦ a ^ ↑q
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by fun_prop

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}
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
  case cont =>
    exact .of_forall fun p ↦ by fun_prop (disch := grind -abstractProof)
  case tendsto =>
    let s := {a : A | IsStrictlyPositive a}
    let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
    have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
    exact hmain (spectrum ℝ a) (by grind) (by grind)

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
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp

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

Goal state before:
pp: case refine_2
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)
q : ℝ × ℝ
⊢ q ∈ Ioi 0 ×ˢ s → Function.uncurry p.rpowIntegrand₀₁ q = g q

Tactic:
intro hq

Goal state after:
case refine_2
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)
q : ℝ × ℝ
hq : q ∈ Ioi 0 ×ˢ s
⊢ Function.uncurry p.rpowIntegrand₀₁ q = g q
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ

Tactic:
simp only [Gammaℝ_def, Gammaℂ_def]

Goal state after:
s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) = 2 * (2 * ↑π) ^ (-s) * Gamma s
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
n : ℕ
hn : 0 < n
⊢ log ↑n = slope f (↑n) (↑n + 1)

Tactic:
rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (by positivity),
      add_sub_cancel_left]

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

Goal state before:
pp: b x : ℝ
⊢ logb b x⁻¹ = -logb b x

Tactic:
by simp [logb, neg_div]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ -log b (↑b ^ (-z)) = z

Tactic:
log_zpow hb,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ - -z = z
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
by
  obtain rfl | hr := hr.eq_or_lt
  · rw [logb_zero, Int.log_zero_right, Int.floor_zero]
  by_cases hb : 1 < b
  · have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
    apply le_antisymm
    · rw [← Int.zpow_le_iff_le_log hb hr, ← rpow_intCast b]
      refine le_of_le_of_eq ?_ (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr)
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.floor_le _)
    · rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]
      exact Int.zpow_log_le_self hb hr
  · 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.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ 0 < b⁻¹

Tactic:
by simpa

Goal state after: