mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
have ⟨t, _, ht, htendsto⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist hf MeasurableSet.univ
    (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x

Tactic:
have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl

Goal state after:
case htc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet {x | f' x ≠ 0}ᶜ
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ NNReal.sqrt x.toNNReal ≤ y.toNNReal ↔ x ≤ y ^ 2

Tactic:
NNReal.sqrt_le_iff_le_sq,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ x.toNNReal ≤ y.toNNReal ^ 2 ↔ x ≤ y ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (↑x + I * ↑√(1 - x ^ 2)) = 1

Tactic:
by
  simp [mul_comm I, normSq_add_mul_I,
    Real.sq_sqrt (x := 1 - x ^ 2) (by nlinarith [abs_le.mp hx])]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ _q • _a₁ ≤ _q • _a₂

Tactic:
← NNRat.cast_smul_eq_nnqsmul ℚ,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ ↑_q • _a₁ ≤ _q • _a₂
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ _q • _a₁ < _q • _a₂

Tactic:
← NNRat.cast_smul_eq_nnqsmul ℚ,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ ↑_q • _a₁ < _q • _a₂
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ SFinite (μ.withDensity f)

Tactic:
wlog hfm : Measurable f generalizing f

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞}, Measurable f → SFinite (μ.withDensity f)
hfm : ¬Measurable f
⊢ SFinite (μ.withDensity f)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
⊢ SFinite (μ.withDensity f)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case zero
r : ℝ
⊢ ↑(r ^ 0) = ↑r ^ 0

Tactic:
simp [*, ofReal_mul, pow_succ]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case succ
r : ℝ
n✝ : ℕ
a✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ (n✝ + 1)) = ↑r ^ (n✝ + 1)

Tactic:
simp [*, ofReal_mul, pow_succ]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ SFinite (μ.withDensity f)

Tactic:
have key := calc
    μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) := by
      simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]
    _ = μ.withDensity (sᶜ.indicator f) + .sum fun _ : ℕ ↦ μ.withDensity (s.indicator 1) := by
      rw [← withDensity_tsum (by measurability)]
      congr 2 with x
      rw [ENNReal.tsum_apply]
      if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
⊢ SFinite (μ.withDensity f)
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
U : ↥(unitary R)
⊢ -↑U ∈ unitary R

Tactic:
simp [mem_iff, star_neg]

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Tactic:
by
  induction n with
  | zero => simp only [pow_zero, pow_one]
  | succ k hk =>
    rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ im (z * ↑r) = im z * r

Tactic:
by
  rw [mul_comm, im_ofReal_mul, mul_comm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) ↑(re z) + (starRingEnd K) (↑(im z) * I) = ↑(re z) - ↑(im z) * I

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) ↑(re z) + (starRingEnd K) ↑(im z) * (starRingEnd K) I = ↑(re z) - ↑(im z) * I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + (y₁ * y₂) • -1

Tactic:
smul_neg,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + -((y₁ * y₂) • 1)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + (starRingEnd K) (I * z)) / 2 = -(I * ((starRingEnd K) z - z) / 2)

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + (starRingEnd K) I * (starRingEnd K) z) / 2 = -(I * ((starRingEnd K) z - z) / 2)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0

Tactic:
simp [normSq_nonneg]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x + y) = (algebraMap ℝ 𝕜) x + (algebraMap ℝ 𝕜) y

Tactic:
by subst h''; exact h.algebraMap.map_add'

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ (fun n ↦ f ((Equiv.neg ℤ) n)) =O[cofinite] fun n ↦ g ((Equiv.neg ℤ) n)

Tactic:
exact hf.comp_tendsto (Equiv.neg ℤ).injective.tendsto_cofinite

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹ = (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m

Tactic:
simp [← mul_sum, mul_comm, inv_pow]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
obtain hx | hx := hx.symm.lt_or_gt

Goal state after:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ x + 1 < rexp x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x + 1 < rexp x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
have := e.continuousAt (e.map_target hb)
      rwa [ContinuousAt, e.rightInvOn hb] at this

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

Goal state before:
pp: ⊢ Continuous sinh

Tactic:
by
  change Continuous fun z => (exp z - exp (-z)) / 2
  fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ⨅ i, ⨅ (_ : 0 < i), Filter.principal ((fun p ↦ p.1⁻¹ * p.2) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}

Tactic:
simp only [dist, preimage_ofPred_eq, norm_eq_groupSeminorm]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / closedBall 1 δ = closedBall x δ

Tactic:
singleton_div_closedBall,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall (x / 1) δ = closedBall x δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ sin x < sin y

Tactic:
rw [← sub_pos, sin_sub_sin]
  have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith
  have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
  positivity

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

Goal state before:
pp: ⊢ (range sin).Infinite

Tactic:
rw [Real.range_sin]
  exact Icc_infinite (by simp)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε + Metric.closedBall (-b) δ = Metric.ball (a + -b) (ε + δ)

Tactic:
ball_add_closedBall hε hδ

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

Goal state before:
pp: ⊢ Function.Periodic sinh (2 * ↑π * I)

Tactic:
convert! sinh_antiperiodic.periodic_two_mul using 1
  ring

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ r • closedBall 0 1 = closedBall x r

Tactic:
by
  rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ JoinedIn F x y

Tactic:
have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
⊢ JoinedIn F x y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : range ⇑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
simp only [range, mem_ofPred_eq] at h₂

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : range ⇑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
· refine congr_arg _ (Subtype.ext ?_)
    norm_num [sub_sub_eq_add_sub, mul_sub]

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
by
  rw [← cauchySeq_shift 1]
  simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
    tsub_zero]
  apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
    ⟨b, eventually_map.mpr <| Eventually.of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add
  refine CauchySeq.neg ?_
  refine cauchySeq_range_of_norm_bounded ?_
    (fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)
  · simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]
    apply Real.uniformContinuous_const_mul.comp_cauchySeq
    simp_rw [sum_range_sub, sub_eq_add_neg]
    exact (Tendsto.cauchySeq hf0).add_const
  · rw [norm_smul, mul_comm]
    exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend (min t₀ t₁)

Tactic:
by rw [min_eq_left h]

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

Goal state before:
pp: x : ℝ
x✝ : x ∈ univ
⊢ log (-rexp x) = x

Tactic:
by rw [log_neg_eq_log, log_exp]

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

Goal state before:
pp: case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log ↑n

Tactic:
← log_neg_eq_log

Goal state after:
case inr.inr
n : ℤ
hn : n < 0
this : 1 ≤ -↑n
⊢ 0 ≤ log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℤ
⊢ 0 ≤ log ↑n

Tactic:
by
  cases lt_trichotomy 0 n with
  | inl hn =>
      have : (1 : ℝ) ≤ n := mod_cast hn
      exact log_nonneg this
  | inr hn =>
      cases hn with
      | inl hn => simp [hn.symm]
      | inr hn =>
          have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
          rw [← log_neg_eq_log]
          exact log_nonneg this

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

Goal state before:
pp: case mp.inr.inl
h : log 0 = 0
⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = -1

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 2 * log √x = log x

pp: x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0

Tactic:
← Nat.cast_two,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ ↑2 * log √x = log x

x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) (↑x.arg * I)

Tactic:
map_mul,

Goal state after:
x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I
    else (starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) ↑x.arg * (starRingEnd ℂ) I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : x.arg ≠ π
⊢ log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)

Tactic:
by
  rw [log_conj_eq_ite, if_neg h]

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

Goal state before:
pp: ⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
by
  rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) (↑x.arg * I)) -
      ↑(Real.log (normSq x)) =
    if x.arg = π then -((starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) (↑x.arg * I))
    else -(↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
map_mul,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I
      else (starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) ↑x.arg * (starRingEnd ℂ) I) -
      ↑(Real.log (normSq x)) =
    if x.arg = π then -((starRingEnd ℂ) ↑(Real.log ‖x‖) + (starRingEnd ℂ) ↑x.arg * (starRingEnd ℂ) I)
    else -(↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π / 2

Tactic:
Real.arcsin_lt_pi_div_two,

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ (-z).im / ‖z‖ < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re

Tactic:
by
  rw [abs_le, arg_le_pi_div_two_iff, neg_pi_div_two_le_arg_iff, ← or_and_left, ← not_le,
    and_not_self_iff, or_false]

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

Goal state before:
pp: ⊢ sin 0 = 0

Tactic:
← coe_zero,

Goal state after:
⊢ (↑0).sin = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ cos 0 = 1

Tactic:
← coe_zero,

Goal state after:
⊢ (↑0).cos = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Tactic:
map_mul,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * (starRingEnd ℂ) ((starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ toReal 0 = 0

Tactic:
← coe_zero,

Goal state after:
⊢ (↑0).toReal = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x * (starRingEnd ℂ) n))

Tactic:
map_mul,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x) * (starRingEnd ℂ) ((starRingEnd ℂ) n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ tan 0 = 0

Tactic:
← coe_zero,

Goal state after:
⊢ (↑0).tan = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal < 0 ↔ θ.sign = -1

Tactic:
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
  grind [sin_nonneg_of_nonneg_of_le_pi, sin_neg_of_neg_of_neg_pi_lt, toReal_mem_Ioc]

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

Goal state before:
pp: a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ 2 • a = 2 • b ↔ a = b

Tactic:
Real.Angle.two_zsmul_eq_iff

Goal state after:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π ↔ a = b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Tactic:
rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ rexp (log b * x) * cos (x * π)) =o[atTop] fun _x ↦ 1 * 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
rw [two_zsmul, ← two_nsmul] at h
  exact abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq h hs h0

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)

Tactic:
exact continuousAt_sign (hs _ hz).1 (hs _ hz).2

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

Goal state before:
pp: k a b : ℝ
ha' : a < b
⊢ (fun t ↦ rexp (a * t) * t ^ k) =o[atTop] fun t ↦ rexp (b * t)

Tactic:
refine (isLittleO_of_tendsto (fun _ h ↦ (Real.exp_ne_zero _ h).elim) ?_)

Goal state after:
k a b : ℝ
ha' : a < b
⊢ Tendsto (fun x ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y