mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: case refine_2
𝕜 : 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
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ F₁.subtype.range

Tactic:
range_subtype

Goal state after:
case refine_2
𝕜 : 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
h : IsStrictMap ⇑u ∧ IsClosed[inst✝⁵] ↑(↑u).range
disj : Disjoint E₁ (↑u).ker
⊢ F₁ ≤ F₁
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint f hf x hx) (efixedPoint f hf y hy)

Tactic:
trans x

Goal state after:
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint f hf x hx) x

α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid x (efixedPoint f hf y hy)
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy)

Tactic:
trans x

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x

α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ∞
hxy : edist x y ≠ ∞
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ∞
⊢ Metric.edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ eval x P) ~[atTop] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
· simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
    exact
      IsLittleO.add_isEquivalent
        (IsLittleO.fun_sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
            _)
        IsEquivalent.refl

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‖₊
⊢ (p.cauchyBound - 1) * ‖a‖₊ ^ p.natDegree / ‖a‖₊ ^ p.natDegree + 1 = p.cauchyBound

Tactic:
by simp [field, tsub_add_cancel_of_le]

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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ⋯
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ closedBall x₀ (a / 2) ⊆ ball x₀ a

Tactic:
exact closedBall_subset_ball <| half_lt_self ha

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

Goal state before:
pp: case neg
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), P.IsRoot y → y < x
⊢ 0 ≤ eval x P

Tactic:
exact (zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc).le

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

Goal state before:
pp: p q : ℂ[X]
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
by_cases hpq : p * q = 0

Goal state after:
case pos
p q : ℂ[X]
hpq : p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

case neg
p q : ℂ[X]
hpq : ¬p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ y ∈ ofDigits '' Set.univ

Tactic:
simp only [Set.image_univ, show y = 1 by grind, Set.mem_range]

Goal state after:
case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ ∃ y, ofDigits y = 1
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3.1415 < π

Tactic:
pi_lower_bound [
    1970 / 1393, 3010 / 1629, 11689 / 5959, 10127 / 5088, 33997 / 17019, 23235 / 11621]

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

Goal state before:
pp: case neg
x : ℝ*
h : ¬∃ r, 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ 0 = stdPart x

Tactic:
push Not at h

Goal state after:
case neg
x : ℝ*
h : ∀ (r : ℝ), 0 ≤ ArchimedeanClass.mk x → stdPart x ≠ r
⊢ 0 = stdPart x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
  exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ (sqrt (x * y), (x + y) / 2).1

Tactic:
exact (le_gm_and_am_le h.le).1

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

Goal state before:
pp: case succ
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
⊢ ((sqrt (k ^ 2 * (x * y))).agmSequences (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2

Tactic:
sqrt_mul,

Goal state after:
case succ
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
⊢ ((sqrt (k ^ 2) * sqrt (x * y)).agmSequences (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p ↦ p * log ↑(↑q - 1)) p + deriv binEntropy p = log (↑q - 1) + log (1 - p) - log p

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_one, differentiableAt_fun_id,
      deriv_mul_const, deriv_id'', one_mul, deriv_binEntropy, add_sub_assoc]

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

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p ↦ p * log ↑(↑q - 1)) p + deriv binEntropy p = log (↑q - 1) + log (1 - p) - log p

pp: case hf
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1)) p

pp: case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
· simp only [Int.cast_sub, Int.cast_natCast, Int.cast_one, differentiableAt_fun_id,
      deriv_mul_const, deriv_id'', one_mul, deriv_binEntropy, add_sub_assoc]

Goal state after:
case hf
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1)) p

case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p ↦ log (↑q - 1) + (log (1 - p) - log p)) (𝓝[<] 1) atBot

Tactic:
apply tendsto_atBot_add_const_left

Goal state after:
q : ℕ
this : (fun p ↦ log (↑q - 1) + log (1 - p) - log p) = fun p ↦ log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun x ↦ log (1 - x) - log x) (𝓝[<] 1) atBot
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))

Tactic:
exact qaryEntropy_strictMonoOn (by rfl)

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

Goal state before:
pp: case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t⁻¹ - (t + x)⁻¹

Tactic:
rw [sub_nonneg]

Goal state after:
case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ (t + x)⁻¹ ≤ t⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ s.Gammaℝ = 0 ↔ ∃ n, s = -(2 * ↑n)

Tactic:
by
  simp [Gammaℝ_def, Complex.Gamma_eq_zero_iff, pi_ne_zero, div_eq_iff (two_ne_zero' ℂ), mul_comm]

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

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (fun s ↦ 2 * ↑π ^ (-s / 2)) 0

Tactic:
exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
      (by fun_prop))

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

Goal state before:
pp: case inr
m n r : ℕ
hr : 0 < r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]

Goal state after:
case inr
m n r : ℕ
hr : 0 < r
⊢ ↑(harmonic r) - log (↑r + 1) < ↑(harmonic r) - log ↑r
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)
⊢ -deriv f 1 = γ

Tactic:
have derivLB (n : ℕ) (hn : 0 < n) : log n ≤ deriv f (n + 1) := by
    refine (le_of_eq ?_).trans <| hc.slope_le_deriv (mem_Ioi.mpr <| Nat.cast_pos.mpr hn)
      (by positivity : _ < (_ : ℝ)) (by linarith) (hder <| by positivity)
    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:
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)
⊢ -deriv f 1 = γ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: ⊢ ↑(Real.pi ^ (1 / 2)) * (-(2 * log 2) - ↑Real.eulerMascheroniConstant) / ↑Real.pi ^ (1 / 2) =
    -2 * log 2 - ↑Real.eulerMascheroniConstant

Tactic:
ofReal_cpow Real.pi_nonneg

Goal state after:
⊢ ↑Real.pi ^ ↑(1 / 2) * (-(2 * log 2) - ↑Real.eulerMascheroniConstant) / ↑Real.pi ^ (1 / 2) =
    -2 * log 2 - ↑Real.eulerMascheroniConstant
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
log_of_right_le_one _ h₁,

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ log b r₂
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
log_of_right_le_one _ h₁,

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ log b r₂
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb |b| x = logb b x

Tactic:
rw [logb, logb, log_abs]

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

Goal state before:
pp: b x : ℝ
⊢ logb b |x| = logb b x

Tactic:
rw [logb, logb, log_abs]

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

Goal state before:
pp: a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log c / log b * (log b / log a) = log c / log a

Tactic:
div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)

Goal state after:
a b c : ℝ
h₁ : b ≠ 0
h₂ : b ≠ 1
h₃ : b ≠ -1
⊢ log c / log a = log c / log a
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹

pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b

Tactic:
· exact zpow_log_le_self hb (inv_pos.mpr hr)

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉ = ↑(Nat.clog (b + 1 + 1) n)

pp: case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n

Tactic:
ceil_logb_natCast (by simp),

Goal state after:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ Int.clog (b + 1 + 1) ↑n = ↑(Nat.clog (b + 1 + 1) n)

case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n
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 →ᵇ ℝ
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
             integrable_of_nnreal]
  simp only [Function.comp_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r

Tactic:
obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r
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:
by
  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.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 1)
⊢ (regularizedHGFunSeries a b).radius = 1

Tactic:
have := FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto (r := 1) ℂ _ (by simp) this

Goal state after:
a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this✝ : Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 1)
this : (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).radius = ↑1⁻¹
⊢ (regularizedHGFunSeries a b).radius = 1
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

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

Tactic:
refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩

Goal state after:
case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a

Tactic:
by
  rw [← integral_deriv_of_contDiffOn_Icc h hab]
  rw [integral_of_le hab, integral_of_le hab]
  apply MeasureTheory.integral_congr_ae
  rw [← restrict_Ioo_eq_restrict_Ioc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,
    integral_of_le hab, restrict_Ioc_eq_restrict_Icc]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ‖∫ (x : ℝ) in Icc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹

Tactic:
rw [integral_symm, ← intervalIntegral.integral_neg]
    simp

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))

pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)

pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n

Tactic:
any_goals positivity

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = log (√(2 * π * ↑n) * (↑n / rexp 1) ^ n)

Tactic:
rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity

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

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i

Tactic:
suffices ∑ i ≤ n, ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * c i) <
      ∑ i ≤ n, ((-1) ^ i * (T ℝ n).eval (node n i)) * ((-1) ^ i * c i) by
    simpa [negOnePow_mul_negOnePow_mul_cancel]

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
⊢ ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
f : i = 0
⊢ ℘[L - l₀] = ℘[L]

Tactic:
rw [L.weierstrassPExcept_of_notMem _ hl₀]

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

Goal state before:
pp: L : PeriodPair
x✝ : ℕ
⊢ L.sumInvPow 0 x✝ = L.G x✝

Tactic:
simp [sumInvPow, G]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 * (↑n + 1) ^ 2 = - -x ^ 2

Tactic:
have := (integerComplement_pow_two_ne_pow_two hx (n + 1 : ℤ))
    aesop

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ (k % 2 + 1 % 2) % 2 = 0

Tactic:
h.2.1

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ (1 + 1 % 2) % 2 = 0