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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞

Tactic:
calc
    (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
      lintegral_mono_ae <| ae_norm_ofReal_f_le_bound h_bound h_lim
    _ < ∞ := by
      rw [← hasFiniteIntegral_iff_ofReal]
      · exact bound_hasFiniteIntegral
      exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ x ∧ 0 ≤ x ^ 2 - x ↔ x = 0 ∨ 1 ≤ x

Tactic:
sq,

Goal state after:
x : ℝ
⊢ 0 ≤ x ∧ 0 ≤ x * x - x ↔ x = 0 ∨ 1 ≤ x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inr
x : ℝ
hx : 0 < x
⊢ x ^ 2 ≤ x ↔ x ≤ 1

Tactic:
sq,

Goal state after:
case inr
x : ℝ
hx : 0 < x
⊢ x * x ≤ x ↔ x ≤ 1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ √(z.re * z.re + z.im * z.im) = √(z.re ^ 2 + z.im ^ 2)

Tactic:
sq,

Goal state after:
z : ℂ
⊢ √(z.re * z.re + z.im * z.im) = √(z.re * z.re + z.im ^ 2)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)

Tactic:
sq,

Goal state after:
z w : ℂ
⊢ dist z w = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) ^ 2)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ dist z w = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) ^ 2)

Tactic:
sq,

Goal state after:
z w : ℂ
⊢ dist z w = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x y : ℝ
⊢ x * x + y * y = x ^ 2 + y ^ 2

Tactic:
sq,

Goal state after:
x y : ℝ
⊢ x * x + y * y = x * x + y ^ 2
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 2 = -1

Tactic:
sq,

Goal state after:
⊢ I * I = -1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

Tactic:
refine lintegral_congr (fun x ↦ ?_)
    rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]
    simp

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
rw [mul_assoc]

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * (b * ‖x‖)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * ‖f‖ * ‖v‖

Tactic:
rw [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * (star U * U) * B = 1

Tactic:
rw [hA₁, mul_one, hB₁]

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
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖↑U‖ ^ 2 = 1

Tactic:
sq,

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖↑U‖ * ‖↑U‖ = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖(x ^ 2 ^ k) ^ 2‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
sq,

Goal state after:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℝ
a : K
⊢ star (r • a) = star r • star a

Tactic:
apply RCLike.ext <;> simp [RCLike.smul_re, RCLike.smul_im]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑n = ↑n

Tactic:
rw [← ofReal_intCast, ofReal_re]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x✝ : ℝ
⊢ 0 ((starRingEnd ℝ) x✝) = -0 x✝

Tactic:
simp only [neg_zero, AddMonoidHom.zero_apply]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
mem_inter_iff,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∧ ↑e y ∈ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ ↑e y ∈ e.target ∧ ↑e.symm (↑e y) ∈ s ∩ f ⁻¹' t

Tactic:
mem_inter_iff,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ ↑e y ∈ e.target ∧ ↑e.symm (↑e y) ∈ s ∧ ↑e.symm (↑e y) ∈ f ⁻¹' t
Module: Mathlib.Analysis.Complex.Asymptotics

Goal state before:
pp: ⊢ (fun x ↦ ‖↑x‖) =ᶠ[cofinite] fun x ↦ ‖↑x‖

Tactic:
filter_upwards with n using by simp

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε

Tactic:
have := add_lt_add hi₁ hi₂

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|
this :
  |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| +
      |(fun n ↦ ∑ i ∈ range n, a i) (max n i) - (fun n ↦ ∑ i ∈ range n, a i) i| <
    ε / 2 + ε / 2
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
h : Q = 0
⊢ False

Tactic:
simp [h] at hQε0

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

Goal state before:
pp: x : ℝ
⊢ ↑(rexp (-x)) = ↑(rexp x)⁻¹

Tactic:
simp [exp_neg]

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 with n ≤ m, 1 / ↑m.factorial = ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial

Tactic:
refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n ∈ range (j - n)

case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n ∈ {m ∈ range j | n ≤ m}

case refine_3
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, a - n + n = a

case refine_4
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), a + n - n = a

case refine_5
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, 1 / ↑a.factorial = 1 / ↑(a - n + n).factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh x * cosh x + sinh x * sinh x = cosh x ^ 2 + sinh x ^ 2

Tactic:
sq,

Goal state after:
x : ℂ
⊢ cosh x * cosh x + sinh x * sinh x = cosh x * cosh x + sinh x ^ 2
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
x✝ : 𝕜
⊢ x✝ = x✝ ^ 1

Tactic:
simp only [pow_one]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
⊢ ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Tactic:
by
  rcases h.exists_pos with ⟨C, C₀, hC⟩
  rw [IsBigOWith_def, eventually_cofinite] at hC
  rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩
  have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'
  refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩
  rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]
  exact fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → E
g : α → F
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
rw [isBigO_iff, exists_eventually_atTop]

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

Goal state before:
pp: case hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1

Tactic:
sq,

Goal state after:
case hab
x : ℝ
hx : |x| ≤ 1
⊢ x * x ≤ 1
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
this : 0 < Q
⊢ ∑ k ∈ range K, abv (f k) - ∑ k ∈ range (max N M + 1), abv (f k) < ε / (4 * Q)

Tactic:
exact (le_abs_self _).trans_lt <|
          hM _ ((Nat.le_succ_of_le (le_max_right _ _)).trans hNMK.le) _ <|
            Nat.le_succ_of_le <| le_max_right _ _

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

Goal state before:
pp: x : ℝ
⊢ rexp x = rexp (x / 2) ^ 2

pp: case hx
x : ℝ
⊢ 0 ≤ rexp x

pp: case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
sq,

Goal state after:
x : ℝ
⊢ rexp x = rexp (x / 2) * rexp (x / 2)

case hx
x : ℝ
⊢ 0 ≤ rexp x

case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
⊢ Tendsto (fun x ↦ rexp x / x ^ n) atTop atTop

Tactic:
by
  refine (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_
  have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
  have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
    eventually_atTop.1
      ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually
        (gt_mem_nhds this))
  simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN
  refine ⟨N, trivial, fun x hx => ?_⟩
  rw [Set.mem_Ioi] at hx
  have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
  rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]
  calc
    x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
    _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
    _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
    _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

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

Goal state before:
pp: n : ℤ
⊢ cos (↑n * π) = (-1) ^ n

Tactic:
simpa using cos_add_int_mul_pi 0 n

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

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ cos x * cos x = sin ?m.18 ^ 2 + cos ?m.18 ^ 2

pp: x : ℝ
⊢ ℝ

Tactic:
sq,

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ cos x * cos x = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

x : ℝ
⊢ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ cos x * cos x = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

pp: x : ℝ
⊢ ℝ

Tactic:
sq,

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ cos x * cos x = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

x : ℝ
⊢ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ sin x * sin x = sin ?m.18 ^ 2 + cos ?m.18 ^ 2

pp: x : ℝ
⊢ ℝ

Tactic:
sq,

Goal state after:
x : ℝ
⊢ cos x = 0 ↔ sin x * sin x = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

x : ℝ
⊢ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ sin x * sin x = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

pp: x : ℝ
⊢ ℝ

Tactic:
sq,

Goal state after:
x : ℝ
⊢ cos x = 0 ↔ sin x * sin x = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

x : ℝ
⊢ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (Icc (-1) 1).Infinite

Tactic:
exact Icc_infinite (by simp)

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ * s = thickening δ s

Tactic:
by rw [mul_comm, mul_ball_one]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
by
  simp [hs.closedBall_mul hδ]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ r ^ n

Tactic:
suffices (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n from
    this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n ↦ ↑n ^ k) =O[atTop] fun n ↦ (r' ^ k) ^ n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ 1 ∈ f ⁻¹' interior (closedBall x (dist y x))

Tactic:
simpa [f]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
⊢ ∃ x, ‖x‖ = c

Tactic:
rcases exists_norm_ne_zero E with ⟨x, hx⟩

Goal state after:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 1 / 2 / cos (π / 6) = 1 / √3

Tactic:
cos_pi_div_six

Goal state after:
⊢ 1 / 2 / (√3 / 2) = 1 / √3
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n ↦ ξ ^ n) (1 - ξ)⁻¹

Tactic:
hasSum_iff_tendsto_nat_of_summable_norm

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i ↦ ‖ξ ^ i‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ sin z = 0 ↔ cos z * cos z = sin ?m.18 ^ 2 + cos ?m.18 ^ 2

pp: z : ℂ
⊢ ℂ

Tactic:
sq,

Goal state after:
z : ℂ
⊢ sin z = 0 ↔ cos z * cos z = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

z : ℂ
⊢ ℂ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ sin z = 0 ↔ cos z * cos z = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

pp: z : ℂ
⊢ ℂ

Tactic:
sq,

Goal state after:
z : ℂ
⊢ sin z = 0 ↔ cos z * cos z = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

z : ℂ
⊢ ℂ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ cos z = 0 ↔ sin z * sin z = sin ?m.18 ^ 2 + cos ?m.18 ^ 2

pp: z : ℂ
⊢ ℂ

Tactic:
sq,

Goal state after:
z : ℂ
⊢ cos z = 0 ↔ sin z * sin z = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

z : ℂ
⊢ ℂ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ cos z = 0 ↔ sin z * sin z = sin ?m.18 * sin ?m.18 + cos ?m.18 ^ 2

pp: z : ℂ
⊢ ℂ

Tactic:
sq,

Goal state after:
z : ℂ
⊢ cos z = 0 ↔ sin z * sin z = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

z : ℂ
⊢ ℂ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
← closure_thickening hδ,

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) =
    infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
← closure_thickening hδ,

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) = thickening (ε + δ) s