mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
x✝¹ : SeminormedAddCommGroup G
x✝ : NormedSpace 𝕜 G
hp : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
⊢ p ≤ projectiveSeminorm

Tactic:
x

Goal state after:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
x✝¹ : SeminormedAddCommGroup G
x✝ : NormedSpace 𝕜 G
hp : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
x : ⨂[𝕜] (i : ι), E i
⊢ p x ≤ projectiveSeminorm x
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_4
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E F) f) x = (lift f.toMultilinearMap) x

Tactic:
by
  simp [LinearIsometryEquiv.ofBounds, liftIsometry]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
h : ‖(lift f.toMultilinearMap) x‖ ≤ ‖f'‖ * injectiveSeminorm x
⊢ ‖f'‖ * injectiveSeminorm x ≤ ‖f‖ * injectiveSeminorm x

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Int

Goal state before:
pp: n : ℤ
⊢ ↑n.toNat + ↑(-n).toNat = ‖n‖

Tactic:
by
  simpa only [NNReal.coe_natCast, NNReal.coe_add] using!
    congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * u k + b k ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k

Tactic:
by gcongr

Goal state after:
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), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ ¬RCLike.re α = 0

Tactic:
exact ne_of_gt hα_pos

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s

Tactic:
have heq : a⁻¹ • s = { t | t * a ∈ s } := by
    ext t
    rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
    rfl

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t | t * a ∈ s}
⊢ IsIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v ∘ fun x ↦ x * a) (a⁻¹ • s) ↔ IsIntegralCurveOn γ v s
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
α : FunSpace t₀ x₀ r L
h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
t : ↑(Icc tmin tmax)
⊢ ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) + ↑r ≤ ↑a - ↑r + ↑r

Tactic:
by gcongr

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax ⋯ t))) (Icc tmin tmax) t

Tactic:
apply hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry
      (α x hx |>.continuous_compProj.continuousOn)
      (fun _ ht' ↦ α x hx |>.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₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := ⋯
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ ∀ x_1 ∈ Icc tmin tmax, (α x hx).compProj x_1 = picard f (↑t₀) x (α x hx).compProj x_1
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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w✝¹ w✝ : ℝ≥0
hr : 0 < r
hpl : ∀ (t₀ : ℝ), IsPicardLindelof (fun x ↦ f) ⟨t₀, ⋯⟩ x₀ a r w✝¹ w✝
x : E
hx : x ∈ closedBall x₀ ↑r
⊢ ∃ α, α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
have ⟨α, hα1, hα2⟩ := (hpl t₀).exists_eq_forall_mem_Icc_hasDerivWithinAt hx

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w✝¹ w✝ : ℝ≥0
hr : 0 < r
hpl : ∀ (t₀ : ℝ), IsPicardLindelof (fun x ↦ f) ⟨t₀, ⋯⟩ x₀ a r w✝¹ w✝
x : E
hx : x ∈ closedBall x₀ ↑r
α : ℝ → E
hα1 : α ↑⟨t₀, ⋯⟩ = x
hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ α, α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
by
  by_cases hP : P = 0
  · simp [hP, IsEquivalent.refl]
  by_cases hQ : Q = 0
  · simp [hQ, IsEquivalent.refl]
  refine
    (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))
  simp [← div_mul_div_comm, zpow_sub₀ hx.ne.symm]

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

Goal state before:
pp: 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.natDegree * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1 ≤
    (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1)) * (‖a‖₊ - 1) / ‖a‖₊ ^ p.natDegree + 1

Tactic:
by gcongr

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

Goal state before:
pp: 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‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree / ‖p.leadingCoeff‖₊ ≤
    ‖∑ x ∈ range p.natDegree, p.coeff x * a ^ x‖₊ / ‖p.leadingCoeff‖₊

Tactic:
by gcongr

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

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ Q ∣ P

Tactic:
rw [← modByMonic_eq_zero_iff_dvd mQ]

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
degR : (P %ₘ Q).degree < Q.degree
⊢ P %ₘ Q = 0
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormOneClass A
⊢ X.supNorm = 1

Tactic:
← monomial_one_one_eq_X,

Goal state after:
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormOneClass A
⊢ ((monomial 1) 1).supNorm = 1
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q ≠ 0
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
j : ℕ
left✝ : j ∈ range (?m.107 + 1)
right✝ : v ((range (?m.107 + 1)).sum ?m.105) ≤ v (?m.105 j)
⊢ v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) * c ^ i ≤ v (p.coeff j * q.coeff (i - j)) * c ^ i

Tactic:
by gcongr

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

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h : Odd P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
rw [Int.negOnePow_odd] at hlc' ⊢
    · push_cast at hlc' ⊢; rw [neg_one_mul] at hlc' ⊢
      have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')
      exact neg_pos.mpr (by simpa using this)
    · simpa
    · simpa [natDegree_comp]

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

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √((⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) ^ 2) ≤ √(⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ ^ 2)

Tactic:
by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

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

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ b * (⌊↑b * y⌋₊ / b) + ↑(Fin.ofNat b ⌊↑b * y⌋₊) = ⌊↑b * y⌋₊

Tactic:
Fin.val_ofNat,

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ b * (⌊↑b * y⌋₊ / b) + ⌊↑b * y⌋₊ % b = ⌊↑b * y⌋₊
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ ↑s

Tactic:
obtain ⟨t, ht⟩ := exists_lt r

Goal state after:
case refine_2
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun n ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun n ↦ i.2
s : ℝ
hs : s > r
t : ℝ
ht : t < r
⊢ ofSeq f ≤ ↑s
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
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
⊢ False

pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False

Tactic:
· obtain rfl : b = 0 := by simpa
    simp at p_nonzero

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : ↑a * x = -↑b
ha : ¬a = 0
⊢ False
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: x✝² x✝¹ : ℕ
x✝ : x✝² < x✝¹
⊢ (2 * ↑x✝¹ + 1)⁻¹ ≤ (2 * ↑x✝² + 1)⁻¹

Tactic:
by gcongr

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

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

Tactic:
rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]

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

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y - (y * x - y * y)
⊢ y * y ≤ y * x

Tactic:
by gcongr

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

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
hxy : x ≤ y
⊢ √(x ^ 2 - 1) ≤ √(y ^ 2 - 1)

Tactic:
by gcongr

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

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y + y * y - y * x
⊢ x * y ≤ x * x

Tactic:
by gcongr

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

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Tactic:
exact binEntropy_neg_of_neg (sub_neg.2 hp)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
h₃' : EqOn (fun a ↦ a ^ p) (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
t : ℝ
ht : t ∈ Ioi 0
⊢ MonotoneOn (cfcₙ ((↑p).rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
exact monotoneOn_cfcₙ_rpowIntegrand₀₁ hp ht

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

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z

Tactic:
refine ⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))
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)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ p * ‖log x‖ ≤ 1 / (sSup ((fun y ↦ ‖log y‖) '' s) + 1) * ‖log x‖

Tactic:
by gcongr

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 : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
⊢ Tendsto (fun t ↦ ∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) F (𝓝 (log (b / a) • V))

Tactic:
by
  rw [Metric.tendsto_nhds]
  intro δ hδ
  set C := |log (b / a)| with hC_def
  set δ' := δ / (C + 1)
  filter_upwards [hpos, huni δ' (by positivity)] with t ht_pos hbound
  have hlog_eq : log (b * t / (a * t)) = log (b / a) := by
    rw [mul_div_mul_right b a (ne_of_gt ht_pos)]
  calc dist (∫ x in a * t..b * t, x⁻¹ • f x) (log (b / a) • V)
    _ = ‖(∫ x in a * t..b * t, x⁻¹ • f x) - log (b / a) • V‖ := dist_eq_norm _ _
    _ = ‖(∫ x in a * t..b * t, x⁻¹ • f x) - log (b * t / (a * t)) • V‖ := by rw [hlog_eq]
    _ ≤ δ' * |log (b * t / (a * t))| :=
        norm_integral_inv_smul_sub_le hf (by positivity) (by positivity) (by positivity) hbound
    _ = δ' * C := by rw [hlog_eq]
    _ = δ * (C / (C + 1)) := by ring
    _ < δ * 1 := mul_lt_mul_of_pos_left ((div_lt_one (by positivity)).2 (lt_add_one C)) hδ
    _ = δ := mul_one δ

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

Goal state before:
pp: case refine_1.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 (fun q ↦ q.1 ^ (p - 1) * q.2) (Ioi 0 ×ˢ s)

pp: case refine_1.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)
⊢ ContinuousOn (fun q ↦ (q.1 + q.2)⁻¹) (Ioi 0 ×ˢ s)

Tactic:
· refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)

Goal state after:
case refine_1.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)
⊢ ContinuousOn (fun q ↦ (q.1 + q.2)⁻¹) (Ioi 0 ×ˢ s)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1) * x / (t + x) = t ^ (p - 1) * x / (t + x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
simp only [Gammaℝ_def]
    ring_nf

Goal state after:
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)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ (f (↑n + 2) - f (↑n + 1)) / (↑n + 2 - (↑n + 1)) = log (↑n + 1)

Tactic:
show n + 2 - (n + 1) = (1 : ℝ) by ring,

Goal state after:
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)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ (f (↑n + 2) - f (↑n + 1)) / 1 = log (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)

Tactic:
have h2 : 0 < (π / a).re := by
    rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
    refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
    contrapose! ha
    rw [ha, zero_re]

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)