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 : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
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))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))

Tactic:
refine tendsto_lintegral_of_dominated_convergence' _ ?_ hb ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
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))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ (n : ℕ), AEMeasurable (fun a ↦ ENNReal.ofReal ‖F n a - f a‖) μ

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
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))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
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))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : x ∈ Ici 0
⊢ normSq ↑√x = x

Tactic:
by rw [normSq_ofReal, Real.mul_self_sqrt hx]

Goal state after:
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:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
    exact smul_lt_smul_of_pos_left (α := ℚ) ha hq

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

Goal state before:
pp: z : ℂ
⊢ (∃ r, z = ↑r) → ↑z.re = z

Tactic:
rintro ⟨r, rfl⟩; simp [ofReal]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
⊢ 𝔼 i ∈ s, f i < 𝔼 _i ∈ s, a

Tactic:
exact expect_lt_expect hle hlt

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
⊢ 𝔼 _i ∈ s, a < 𝔼 i ∈ s, f i

Tactic:
exact expect_lt_expect hle hlt

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ (f.comp 0) x✝ = 0 x✝

Tactic:
exact map_zero f

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ ℑ x = 0

Tactic:
rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: z : ℂ
| ↑(ℜ z)

Tactic:
rw [← re_add_im z]

Goal state after:
z : ℂ
| ↑(ℜ (↑z.re + ↑z.im * I))
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.source.domRestrict ↑f) f.target ⋯)

Tactic:
exact h.continuous

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
⊢ (AddMonoidHom.id ℝ) 0 = 0

Tactic:
by simp only [map_zero]

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
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x) ↔ ContinuousWithinAt (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s) (↑e.symm x)

Tactic:
inter_comm,

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
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x) ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s ∩ e.source) (↑e.symm x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        z‖ =
    ‖z‖

Tactic:
rw [← re_add_im z]

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        (↑(re z) + ↑(im z) * I)‖ =
    ‖↑(re z) + ↑(im z) * I‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := K)
  · simp [h, im_eq_zero]
  · have : (I : K) ≠ 0 := fun _ ↦ by simp_all
    rw [← mul_right_inj' (neg_ne_zero.mpr this)]
    convert! norm_le_re_iff_eq_norm (z := -I * z) using 2
    all_goals simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f') ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ g')

Tactic:
by
  simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
⊢ f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0

Tactic:
simp only [← principal_univ, isLittleO_principal, mem_univ, forall_true_left]

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

Goal state before:
pp: x : ℂ
⊢ cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cosh x)

Tactic:
rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]

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

Goal state before:
pp: x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I

Tactic:
apply Complex.ext <;> simp

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

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
rw [hj, sum_range_add_sub_sum_range]

Goal state after:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖∑ k ∈ range k, x ^ (n + k) / ↑(n + k).factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin (2 * x) = 2 * sin x * cos x

Tactic:
rw [two_mul, sin_add, two_mul, add_mul, mul_comm]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ range j with n ≤ k, x ^ k / ↑k.factorial‖ ≤ ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / ↑k.factorial

Tactic:
refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range j with n ≤ i, ‖x ^ i / ↑i.factorial‖ = ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / ↑k.factorial
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x ↦ f x * g x) =O[l] h ↔ g =O[l] fun x ↦ h x / f x

Tactic:
isBigO_iff_isBigOWith,

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c, IsBigOWith c l (fun x ↦ f x * g x) h) ↔ g =O[l] fun x ↦ h x / f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ |sin x| = sin |x|

Tactic:
rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]

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

Goal state before:
pp: ⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1

Tactic:
simpa [sq, mul_self_eq_one_iff] using sin_sq_add_cos_sq (π / 2)

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
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ x + y ∈ sphere x r

Tactic:
by simpa using hy

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
⊢ Tendsto (fun n ↦ v (1 + a ^ n)) atTop (𝓝 1)

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le (by simpa using h_sub) (by simpa using h_add)
    (fun n ↦ le_trans (by simp) (v.le_add _ _))
    (fun n ↦ le_trans (v.add_le _ _) (by simp))

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

Goal state before:
pp: ⊢ sin (π / 3) = √3 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]
  congr
  ring

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

Goal state before:
pp: ⊢ cos (π / 5) = (1 + √5) / 4

Tactic:
set c := cos (π / 5)

Goal state after:
c : ℝ := cos (π / 5)
⊢ c = (1 + √5) / 4
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 +ᵥ closedBall 0 ‖r‖ = closedBall x r

Tactic:
Real.norm_of_nonneg hr,

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ closedBall 0 r = closedBall x r
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
K : Set X
i : ι
hi : {f | MapsTo ⇑f (K, i).1 (U (K, i).2)} ⊆ s
hK : IsCompact (K, i).1
hpi : p (K, i).2
f : C(X, Y)
hf : MapsTo (⇑f) K (interior (U i))
⊢ f ∈ s

Tactic:
exact hi <| hf.mono_right interior_subset

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
a : ℝ
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))
  rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
  refine ⟨ball 0 |a|, isOpen_ball, ?_⟩
  ext ⟨x, hx⟩
  obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
  simp [ha, Real.dist_eq, abs_mul, (by norm_cast : |(k : ℝ)| < 1 ↔ |k| < 1)]

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

Goal state before:
pp: case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|

Tactic:
rw [abs_eq_neg_self.mpr hp.le] at hx

Goal state after:
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ -p / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x

Tactic:
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin] <;> simp [sub_eq_add_neg]

Goal state after:
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π

case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
· rw [← exp_mul_I, ofReal_exp, toIocMod]
    push_cast
    rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]

Goal state after:
z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y

Tactic:
← exp_lt_exp,

Goal state after:
x y : ℝ
hx : 0 < x
h : x < y
⊢ rexp (log x) < rexp (log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
← exp_lt_exp,

Goal state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ rexp (log x) < rexp (log y) ↔ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ log x < y ↔ x < rexp y

Tactic:
← exp_lt_exp,

Goal state after:
x y : ℝ
hx : 0 < x
⊢ rexp (log x) < rexp y ↔ x < rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ x < log y ↔ rexp x < y

Tactic:
← exp_lt_exp,

Goal state after:
x y : ℝ
hy : 0 < y
⊢ rexp x < rexp (log y) ↔ rexp x < y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = -(π / 2)

Tactic:
rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = -Real.arccos (Real.cos (-z.arg))

Tactic:
Real.arccos_cos,

Goal state after:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = - -z.arg

case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 • ↑π = 0

Tactic:
simp [← intCast_mul_eq_zsmul]

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

Goal state before:
pp: a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x ↦ x ^ n / (a * rexp x + b)) ∘ log =ᶠ[atTop] fun x ↦ log x ^ n / (a * x + b)

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

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

Goal state before:
pp: z : ℂ
⊢ ∃ n, log (cexp z) = z + ↑n * (2 * ↑π * I)

Tactic:
by
  rw [← exp_eq_exp_iff_exists_int, exp_log]
  exact exp_ne_zero z

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

Goal state before:
pp: case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x

Tactic:
have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop
    refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)
    exact continuousAt_arg h

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

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
exact Real.log_pos this

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

Goal state before:
pp: x : ℂ
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
by
  rw [norm_eq_one_iff]
  constructor
  · rintro ⟨θ, rfl⟩
    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
    · convert! toIocMod_mem_Ioc _ _ _
      ring
    · rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
  · rintro ⟨θ, _, rfl⟩
    exact ⟨θ, rfl⟩

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 ≤ z.re

Tactic:
← not_le,

Goal state after:
z : ℂ
⊢ 0 ≤ z.re ∨ 0 ≤ z.im ∧ ¬0 ≤ z.im ↔ 0 ≤ z.re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ Real.sin θ.toReal = θ.sin

Tactic:
conv_rhs => rw [← coe_toReal θ, sin_coe]

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

Goal state before:
pp: θ : Angle
⊢ |θ.toReal| = π / 2 ↔ 0 = θ.cos

Tactic:
rw [@eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]

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

Goal state before:
pp: case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z | 0 ≤ z.im} z

Tactic:
refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds

Goal state after:
case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : θ.sign = ψ.sign
⊢ θ = ψ ↔ |θ.toReal| = |ψ.toReal|

Tactic:
simpa [h] using @eq_iff_sign_eq_and_abs_toReal_eq θ ψ

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

Goal state before:
pp: case inl
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

pp: case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

pp: case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
case inl => -- b < 0
    simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
    rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
    refine IsLittleO.mul_isBigO ?exp ?cos
    case exp =>
      rw [isLittleO_const_iff one_ne_zero]
      refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
      rw [← log_neg_eq_log, log_neg_iff (by linarith)]
      linarith
    case cos =>
      rw [isBigO_iff]
      exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Goal state after:
case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
· subst h
      simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
      exact Or.inr ⟨rfl, hyp.symm⟩

Goal state after:
case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]

Goal state after:
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x‖ ^ y.re = x ^ y.re

Tactic:
Complex.norm_of_nonneg hx.le

Goal state after:
x : ℝ
hx : 0 < x
y : ℂ
⊢ x ^ y.re = x ^ y.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

pp: case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im

pp: case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π

Tactic:
Complex.ofReal_cpow hx

Goal state after:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (↑x ^ ↑y) ^ ↑z = (↑x ^ ↑y) ^ ↑z

case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ y * x ^ 1 = x ^ y * x

Tactic:
rpow_one

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ y * x = x ^ y * x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ 1 * x ^ y = x * x ^ y

Tactic:
rpow_one

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x * x ^ y = x * x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ y / x ^ 1 = x ^ y / x

Tactic:
rpow_one

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ y / x = x ^ y / x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x ^ 1 / x ^ y = x / x ^ y

Tactic:
rpow_one

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : 1 - y ≠ 0
⊢ x / x ^ y = x / x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x⁻¹ ^ 1 = x⁻¹

Tactic:
rpow_one

Goal state after:
x : ℝ
⊢ x⁻¹ = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ 1 = x

Tactic:
rpow_one

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ x ^ 1 = x

Tactic:
rpow_one

Goal state after:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
· exact continuousAt_const_cpow ha

Goal state after: