mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: 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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
e : E
⊢ 0 • e = 0

Tactic:
by simp [zero_smul]

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

Goal state before:
pp: 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
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
e : ↥K⟮x⟯
⊢ 0 • e = 0

Tactic:
by simp [zero_smul]

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 R : { P // IsLprojection X P }
h₁ : ↑P = ↑(P ⊓ Q)
h₂ : ↑Q = ↑(Q ⊓ R)
⊢ ↑P = ↑(P ⊓ R)

Tactic:
simp only [coe_inf] at h₁ h₂ ⊢

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P = ↑P * ↑R
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 R : { P // IsLprojection X P }
h₁ : ↑P = ↑P * ↑Q
h₂ : ↑Q = ↑Q * ↑R
⊢ ↑P = ↑P * ↑R

Tactic:
rw [h₁, mul_assoc, ← h₂]

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
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
π'_quot : IsOpenQuotientMap ⇑π'
u_restr_eq : u.domRestrict A = v.domRestrict B ∘SL π'
⊢ IsStrictMap (⇑v ∘ ⇑π) ∧ IsClosed[inst✝³] ↑(↑v).range ↔ IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range

Tactic:
π_quot.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
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
comap_B : comap (↑π) B = A
A_mapsTo_B : MapsTo ⇑π ↑A ↑B
B_closed : IsClosed[QuotientModule.Quotient.topologicalSpace N] ↑B
step4_output :
  IsStrictMap ⇑v ∧ IsClosed[inst✝³] ↑(↑v).range ↔
    IsStrictMap ⇑(v.domRestrict B) ∧ IsClosed[inst✝³] ↑(↑(v.domRestrict B)).range
range_eq : (↑v).range = (↑u).range
range_restr_eq : (↑(v.domRestrict B)).range = (↑(u.domRestrict A)).range
π' : ↥A →L[𝕜] ↥B := π.restrict A_mapsTo_B
π'_quot : IsOpenQuotientMap ⇑π'
u_restr_eq : u.domRestrict A = v.domRestrict B ∘SL π'
⊢ IsStrictMap (⇑v ∘ ⇑π) ∧ IsClosed[inst✝³] ↑(↑v).range ↔ IsStrictMap (⇑v ∘ ⇑π) ∧ IsClosed[inst✝³] ↑(↑v).range
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
⊢ x = y ∨ edist x y = ∞

Tactic:
by
  refine or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_
  simpa only [hx.eq, edist_self, add_zero, ENNReal.zero_div] using hf.edist_le_of_fixedPoint h hy

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 hP : P = 0
  · simp [hP]
  · refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
    · exact leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)
    · exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inr
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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
have h_supp_p : p.support.Nonempty := support_nonempty.mpr <| left_ne_zero_of_mul hpq

Goal state after:
case inr
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
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q
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 (i + 1)
right✝ : v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) ≤ v (p.coeff j * q.coeff (i - j))
hp_le : v (p.coeff j) * c ^ j ≤ gaussNorm v c p
hq_le : v (q.coeff (i - j)) * c ^ (i - j) ≤ gaussNorm v c q
⊢ v (p.coeff j) * c ^ j * (v (q.coeff (i - j)) * c ^ (i - j)) ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i

Tactic:
have := p.gaussNorm_nonneg v hc

Goal state after:
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 (i + 1)
right✝ : v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) ≤ v (p.coeff j * q.coeff (i - j))
hp_le : v (p.coeff j) * c ^ j ≤ gaussNorm v c p
hq_le : v (q.coeff (i - j)) * c ^ (i - j) ≤ gaussNorm v c q
this : 0 ≤ gaussNorm v c p
⊢ v (p.coeff j) * c ^ j * (v (q.coeff (i - j)) * c ^ (i - j)) ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i
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
h : Odd P.natDegree
hlc' : 0 ≤ -1 * (P.comp (-X)).leadingCoeff
⊢ 0 < -1 * eval x P

Tactic:
rw [neg_one_mul] at hlc' ⊢

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Odd P.natDegree
hlc' : 0 ≤ -(P.comp (-X)).leadingCoeff
⊢ 0 < -eval x P
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
z : ℂ
h : ¬z = 0
⊢ rexp (log ‖z‖) = ‖z‖

Tactic:
simp [h, exp_log]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
⊢ gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
classical
  refine Real.iSup_le ?_ ?_
  · intro t
    obtain ⟨k, hk, hsum⟩ := IsNonarchimedean.finset_image_add vZero vNonneg vna
      (fun a ↦ coeff a.1 f * coeff a.2 g) (Finset.antidiagonal t)
    have hk' : k.1 + k.2 = t := by
      simpa [Finset.mem_antidiagonal] using hk (Finset.nonempty_def.mpr ⟨(t, 0), by simp⟩)
    have hprod : t.prod (c · ^ ·) = k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·) := by
      simp [← hk', Finsupp.prod_add_index' (h := (c · ^ ·)) (by grind) (by grind)]
    rw [hprod]
    refine (mul_le_mul hsum (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1) (c_prod_nonneg c hc k.2))
      (vNonneg _)).trans ?_
    have : v ((coeff k.1) f * (coeff k.2) g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) ≤
        (v (coeff k.1 f) * k.1.prod (c · ^ ·)) * (v (coeff k.2 g) * k.2.prod (c · ^ ·)) := by
      calc
      _ ≤ v (coeff k.1 f) * v (coeff k.2 g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) :=
        mul_le_mul (vMul _ _) (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1)
          (c_prod_nonneg c hc k.2)) (mul_nonneg (vNonneg _) (vNonneg _))
      _ = _ := by ring
    exact this.trans (mul_le_mul (le_gaussNorm v c f hbfd k.1) (le_gaussNorm v c g hbgd k.2)
      (mul_nonneg (vNonneg _) (c_prod_nonneg c hc k.2)) (gaussNorm_nonneg v c f vNonneg))
  · exact mul_nonneg (gaussNorm_nonneg v c f vNonneg) (gaussNorm_nonneg v c g vNonneg)

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

Goal state before:
pp: case a.refine_1
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‖
⊢ Integrable (fun θ ↦ ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (uIoc 0 (2 * π)))

pp: case a.refine_2
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‖
⊢ Integrable ((fun x ↦ x ^ 2) ∘ fun θ ↦ ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (uIoc 0 (2 * π)))

Tactic:
· exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

Goal state after:
case a.refine_2
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‖
⊢ Integrable ((fun x ↦ x ^ 2) ∘ fun θ ↦ ‖eval (circleMap 0 1 θ) p‖) (volume.restrict (uIoc 0 (2 * π)))
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)

Tactic:
rwa [cast_one]

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

Goal state before:
pp: case hf0
⊢ Tendsto (fun x ↦ 2 * ↑x) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two

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

Goal state before:
pp: 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
⊢ |y| < 1

Tactic:
abs_lt

Goal state after:
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
⊢ -1 < y ∧ y < 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
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]
    exact ConcaveOn.congr (concaveOn_id (convex_Ici _)) nnrpow_one_eqOn.symm

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
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
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
x : ℝ
hx : x ∈ uIoc a b
hx_pos : 0 < x
⊢ |x⁻¹| * ‖f x - V‖ ≤ x⁻¹ * δ

Tactic:
abs_of_pos (inv_pos.2 hx_pos)

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
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
x : ℝ
hx : x ∈ uIoc a b
hx_pos : 0 < x
⊢ x⁻¹ * ‖f x - V‖ ≤ x⁻¹ * δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ (-1) ≤ a • 1 ^ (-1) + b • r ^ (-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)

Tactic:
by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this

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

Goal state before:
pp: case inl
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_zero : t = 0
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ s.Gammaℝ ≠ 0

Tactic:
apply mul_ne_zero

Goal state after:
case ha
s : ℂ
hs : 0 < s.re
⊢ ↑π ^ (-s / 2) ≠ 0

case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
← log_div (by positivity) (by positivity),

Goal state after:
n : ℕ
⊢ 0 < ↑(↑(n + 1))⁻¹ - log ((↑(n + 1) + 1) / (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ ↑(harmonic (n + 1)) - log ↑(n + 1) < ↑(harmonic n) - log ↑n
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ ↑(↑(n + 1))⁻¹ < log ↑(n + 1) - log ↑n

Tactic:
← log_div (by positivity) (by positivity),

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

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

Tactic:
mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)),

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((s + 1).Gammaℝ * (1 - s).Gammaℝ)
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)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
hn : 0 < n
⊢ log ↑n ≤ deriv f (↑n + 1)

Tactic:
exact derivLB n hn

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

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ SurjOn (logb b) (Iio 0) univ

Tactic:
intro x _
  use -b ^ x
  constructor
  · simp only [Right.neg_neg_iff, Set.mem_Iio]
    apply rpow_pos_of_pos b_pos
  · rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ ConcaveOn ℝ (Ici 0) (cfc (p.rpowIntegrand₀₁ t))

Tactic:
have h₁ : (Ici (0 : A)).EqOn (cfc (rpowIntegrand₀₁ p t))
      (fun x : A =>
        algebraMap ℝ A (t ^ (p - 1)) - t ^ p • Ring.inverse (algebraMap ℝ A t + x)) := by
    intro x hx
    rw [rpowIntegrand₀₁_eq_sub (by grind) ht]
    have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)
    have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
    have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
    have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
    rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
h₁ :
  EqOn (cfc (p.rpowIntegrand₀₁ t))
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) (Ici 0)
⊢ ConcaveOn ℝ (Ici 0) (cfc (p.rpowIntegrand₀₁ t))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsOpenPosMeasure
⊢ ∀ (U : Set ↑(sphere 0 1)), IsOpen U → U.Nonempty → μ.toSphere U ≠ 0

Tactic:
by
    nontriviality E using not_nonempty_iff_eq_empty
    rintro U hUo hU
    rw [μ.toSphere_apply' hUo.measurableSet]
    apply mul_ne_zero (by simp [Module.finrank_pos.ne'])
    exact isOpen_Ioo.smul_sphere one_ne_zero (by simp) hUo |>.measure_ne_zero _ (by simpa)

Goal state after:
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
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ (fun a ↦ μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (a ^ (p - 1))) =ᵐ[volume.restrict (Ioi 0)] fun a ↦
    μ {a_1 | a < f a_1} * ENNReal.ofReal (a ^ (p - 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
α β : ℚ
⊢ ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice ↔ α.den = 1 ∧ β.den = 1

Tactic:
by
  refine ⟨fun H ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · obtain ⟨m, n, e⟩ := mem_lattice.mp H
    have := LinearIndependent.pair_iff.mp L.indep (m - α) (n - β)
      (by simp; linear_combination e)
    simp only [sub_eq_zero] at this
    norm_cast at this
    aesop
  · lift α to ℤ using h₁
    lift β to ℤ using h₂
    simp only [Rat.cast_intCast, ← zsmul_eq_mul]
    exact add_mem (Submodule.smul_mem _ _ L.ω₁_mem_lattice)
      (Submodule.smul_mem _ _ L.ω₂_mem_lattice)

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

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
have ⟨c, hc1, hc2⟩ := nthRoot.always_exists n a
  calc a < (c + 1) ^ (n + 1) := hc2
    _ ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
      exact nthRoot.lt_pow_go_succ_aux0 hb
    _ ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr

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

Goal state before:
pp: n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

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

Goal state before:
pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0

Tactic:
· exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

Goal state after: