mathlib-initiative/mathlib-tactics huggingface dataset:
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
S_compl_A : IsCompl S A
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A)

Tactic:
have : FiniteDimensional 𝕜 S := .of_fg <| A_cofg.fg_of_isCompl S_compl_A.symm

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
S_compl_A : IsCompl S A
this : FiniteDimensional 𝕜 ↥S
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A)
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
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
by_cases! Subsingleton V

Goal state after:
case pos
𝕜 : 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✝ : Subsingleton V
⊢ ∃ U, f = U.conjStarAlgEquiv

case neg
𝕜 : 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
⊢ ∃ U, f = U.conjStarAlgEquiv
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✝¹ : Subsingleton V
h✝ : Subsingleton W
x✝ : V
⊢ ‖0 x✝‖ = ‖x✝‖

Tactic:
by simp [Subsingleton.eq_zero (α := V), Subsingleton.eq_zero (α := W)]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hy : IsFixedPt f y
⊢ dist x y ≤ dist x (f x) / (1 - ↑K)

Tactic:
simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
⊢ IsFixedPt f (fixedPoint f^[n] hf)

Tactic:
set x := hf.fixedPoint f^[n]
  have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
  have := hf.toLipschitzWith.dist_le_mul x (f x)
  rw [← iterate_succ_apply, iterate_succ_apply', hx] at this
  contrapose! this
  simpa using mul_lt_mul_of_pos_right (NNReal.coe_lt_one.2 hf.left) <| dist_pos.2 (Ne.symm this)

Goal state after:
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)
⊢ ‖α.toFun t - α.toFun t₀‖ + ‖α.toFun t₀ - x₀‖ ≤ ↑L * |↑t - ↑t₀| + ↑r

Tactic:
apply add_le_add _ <| mem_closedBall_iff_norm.mp α.mem_closedBall₀

Goal state after:
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)
⊢ ‖α.toFun t - α.toFun t₀‖ ≤ ↑L * |↑t - ↑t₀|
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P) atTop atTop
this : 0 < P.natDegree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
natDegree_pos_iff_degree_pos

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
⊢ ∃ ε', ∃ (hε' : 0 < ε'), IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a' r' L K

Tactic:
have ha'r' : (0 : ℝ) < a' - r' := by simp only [sub_pos, NNReal.coe_lt_coe, hr]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < ↑a' - ↑r'
⊢ ∃ ε', ∃ (hε' : 0 < ε'), IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a' r' L K
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
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
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
this :
  v ((coeff k.1) f * (coeff k.2) g) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) ≤
    (v ((coeff k.1) f) * k.1.prod fun x1 x2 ↦ c x1 ^ x2) * (v ((coeff k.2) g) * k.2.prod fun x1 x2 ↦ c x1 ^ x2)
⊢ v ((coeff k.1) f * (coeff k.2) g) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) ≤
    gaussNorm v c f * gaussNorm v c g

Tactic:
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))

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

Goal state before:
pp: α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
⊢ f (a + b) = max (f a) (f b)

Tactic:
apply le_antisymm (na a b)

Goal state after:
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
⊢ max (f a) (f b) ≤ f (a + b)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: z : ℂ
this : log (X - C z).mahlerMeasure = log⁺ ‖z‖
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖

Tactic:
apply_fun exp at this

Goal state after:
z : ℂ
this : rexp (log (X - C z).mahlerMeasure) = rexp (log⁺ ‖z‖)
⊢ (X - C z).mahlerMeasure = max 1 ‖z‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : log p.mahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
apply_fun exp at this

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : rexp (log p.mahlerMeasure) = rexp (log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum)
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑(-q) + (↑q + x))

Tactic:
rwa [cast_neg, neg_add_cancel_left]

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

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ n * x)
⊢ Irrational x

Tactic:
exact h.mul_cases.elim (of_pow n) id

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

Goal state before:
pp: m : ℤ
x : ℝ
⊢ Irrational (x * ↑↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
irrational_mul_ratCast_iff,

Goal state after:
m : ℤ
x : ℝ
⊢ ↑m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
by
  rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]

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

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x * ↑↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
irrational_mul_ratCast_iff,

Goal state after:
n : ℕ
x : ℝ
⊢ ↑n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: q : ℚ
x : ℝ
⊢ Irrational (x * ↑q⁻¹) ↔ q ≠ 0 ∧ Irrational x

Tactic:
irrational_mul_ratCast_iff,

Goal state after:
q : ℚ
x : ℝ
⊢ q⁻¹ ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x.agm y ≤ y

Tactic:
apply (agm_le_agmSequences_snd 0).trans

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ (x.agmSequences y 0).2 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ artanh (tanh x) = x

Tactic:
rw [artanh, ← exp_eq_exp, exp_log (sqrt_pos_of_pos h),
    ← sq_eq_sq₀ (le_of_lt <| sqrt_pos_of_pos h) (exp_nonneg x),
    sq_sqrt (le_of_lt h), tanh_eq, exp_neg]

Goal state after:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) / (1 - (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) = rexp x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ p = 0 ∨ p = 1 → binEntropy p = 0

Tactic:
by rintro (rfl | rfl) <;> simp

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

Goal state before:
pp: ⊢ Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
apply Filter.tendsto_atTop_add_left_of_le' (𝓝[>] 0) (log (1 / 2) : ℝ)
  · have h₁ : (0 : ℝ) < 1 / 2 := by simp
    filter_upwards [Ioc_mem_nhdsGT h₁] with p hx
    gcongr
    linarith [hx.2]
  · apply tendsto_neg_atTop_iff.mpr tendsto_log_nhdsGT_zero

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

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 = 2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
by
  rw [recursion' (n + 1)]
  push_cast
  ring

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

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
this : ∀ᶠ (a_1 : ℕ) in atTop, ↑a ^ (2 * a_1 + 1) / ↑a_1 ! < 1 / 2
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! < 1 / 2
⊢ ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1

Tactic:
lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
this : ∀ᶠ (a_1 : ℕ) in atTop, ↑a ^ (2 * a_1 + 1) / ↑a_1 ! < 1 / 2
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * 2 < 1
⊢ ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
⊢ uIcc (c * a) (c * b) ⊆ Ioi 0

Tactic:
by simp [uIcc, Icc_subset_Ioi_iff, mul_pos hc ha,
        mul_pos hc hb]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case a
n : ℕ
f : ℝ → ℝ := ⋯
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)
⊢ γ ≤ -deriv f 1

Tactic:
apply le_of_tendsto tendsto_harmonic_sub_log_add_one

Goal state after:
case a
n : ℕ
f : ℝ → ℝ := ⋯
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)
⊢ ∀ᶠ (c : ℕ) in atTop, ↑(harmonic c) - log (↑c + 1) ≤ -deriv f 1
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ HasDerivAt f ↑g' ↑s

Tactic:
by
  refine HasDerivAt.congr_deriv hf.hasDerivAt ?_
  rw [← (funext hfg ▸ hf.hasDerivAt.comp_ofReal.deriv :)]
  exact hg.ofReal_comp.deriv

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

Goal state before:
pp: case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x

Tactic:
· rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

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

Goal state before:
pp: ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |(ε.mulExpNegMulSq ∘ ⇑g) x| ≤ ‖g‖

Tactic:
simp only [Function.comp_apply, mulExpNegMulSq, abs_mul, abs_exp]

Goal state after:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |g x| * rexp (-(ε * g x * g x)) ≤ ‖g‖
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ ⇑f) μ

Tactic:
by
  refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩
  simp only [hasFiniteIntegral_iff_enorm, Function.comp_apply, NNReal.enorm_eq]
  exact lintegral_lt_top_of_nnreal _ f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (const X c - f) x ∂μ = μ.real Set.univ • c - ∫ (x : X), f x ∂μ

Tactic:
by
  simp [integral_sub (integrable_const c) (f.integrable _)]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ
  have : IsCompact (closure s ∩ t) := hs.inter_right ht
  refine this.of_isClosed_subset isClosed_closure ?_
  refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
  rw [IsClosed.closure_eq ht]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)

Goal state after:
case inr
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Tactic:
obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x ↦ ↑↑x))
⊢ ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ log (stirlingSeq n) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * ↑n * (↑n + 1))

Tactic:
rcases n with (_ | n)

Goal state after:
case zero
⊢ log (stirlingSeq 0) - log (stirlingSeq (0 + 1)) ≤ 1 / (12 * ↑0 * (↑0 + 1))

case succ
n : ℕ
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑n) ∂measureT = π / 2

Tactic:
rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind), sub_self,
    integral_eval_T_real_measureT_zero, zero_add]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case e'_2
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)

Tactic:
simp_rw [sum_mul]
    congr! 1 with i hi
    rw [← Complex.exp_nat_mul, ← Complex.exp_add]
    grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case e'_2
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)

pp: case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑k / ↑n * ↑π * I) ^ n - 1

Tactic:
· simp_rw [sum_mul]
    congr! 1 with i hi
    rw [← Complex.exp_nat_mul, ← Complex.exp_add]
    grind

Goal state after:
case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑k / ↑n * ↑π * I) ^ n - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
⊢ ↑n ≤ ↑d

Tactic:
replace hP := ge_of_eq hP

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : 2 ^ (n - 1) ≤ P.leadingCoeff
⊢ ↑n ≤ ↑d
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ |x|
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
wlog! h : 0 ≤ x

Goal state after:
case inr
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ}, 1 ≤ |x| → 0 ≤ x → 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 1 ≤ |eval x (T ℝ n)|

n : ℤ
x : ℝ
hx : 1 ≤ |x|
h : 0 ≤ x
⊢ 1 ≤ |eval x (T ℝ n)|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
⊢ 1 < |eval x (T ℝ n)|

Tactic:
wlog! h : 0 ≤ x

Goal state after:
case inr
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < |x| → 0 ≤ x → 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 1 < |eval x (T ℝ n)|

n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_1
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀

pp: case refine_2
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀ ≠ 0

pp: case refine_3
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) z

Tactic:
· have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)
      suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop
      by_cases hl₀ : l₀ = 0
      · simpa [hl₀] using analyticAt_const
      · fun_prop (disch := simpa)

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀ ≠ 0

case refine_3
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: Z : Set ℂ
hZ : IsCompact Z
⊢ ∃ u, Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j

Tactic:
have hf : ContinuousOn (fun x : ℂ => ‖-x ^ 2‖) Z := by
    fun_prop

Goal state after:
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
⊢ ∃ u, Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j