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 : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
⊢ Tendsto (fun n ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖)) →
    (∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)) → ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
tendsto_norm

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
tendsto_norm : Tendsto (fun n ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))
⊢ (∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)) → ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
a : α
⊢ Tendsto (fun n ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ) → (∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a) → ‖f' a‖ₑ ≤ bound' a

Tactic:
tendsto_norm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
a : α
tendsto_norm : Tendsto (fun n ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ)
⊢ (∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a) → ‖f' a‖ₑ ≤ bound' a
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℂ
⊢ (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w

Tactic:
by
  simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
by_cases h : ‖x‖ = 0

Goal state after:
case pos
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

case neg
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst✝⁷ : UniformSpace E₁
inst✝⁶ : UniformSpace E₂
inst✝⁵ : Ring E₁
inst✝⁴ : IsUniformAddGroup E₁
inst✝³ : Algebra R E₁
inst✝² : Ring E₂
inst✝¹ : IsUniformAddGroup E₂
inst✝ : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑e
h₂ : Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
⊢ Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] e.invFun

Tactic:
by dsimp; fun_prop

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

Goal state before:
pp: ⊢ (LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe = !![1, 0; 0, -1]

Tactic:
ext i j

Goal state after:
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) i j = !![1, 0; 0, -1] i j
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
by
  rcases eq_or_ne z 0 with (rfl | h₀)
  · simp
  · apply inv_eq_of_mul_eq_one_right
    rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]
    simpa

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖↑‖x‖ / x‖ = 1 ∧ ↑‖x‖ = ↑‖x‖ / x * x

Tactic:
by simp [norm_ne_zero_iff.2, hx]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖x / ↑‖x‖‖ = 1 ∧ x / ↑‖x‖ * ↑‖x‖ = x

Tactic:
by simp [norm_ne_zero_iff.2, hx]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ im ↑n = 0

Tactic:
rw [← ofReal_natCast, ofReal_im]

Goal state after:
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
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ e.source

Tactic:
rw [h]
      exact mem_univ _

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ re z < 0 ∧ im z = 0

Tactic:
by
  simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)

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

Goal state before:
pp: case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩

Goal state after:
case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < ↑n
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ (f'' =O[l] fun _x ↦ c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖

Tactic:
refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩
  rintro ⟨hcf, hf⟩
  rcases eq_or_ne c 0 with (hc | hc)
  exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc]

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

Goal state before:
pp: α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
⊢ f =O[l] g

Tactic:
obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists

Goal state after:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
C : ℝ
_hC₀ : C > 0
hC : IsBigOWith C l (f ^ n) (g ^ n)
c : ℝ
hc₀ : 0 ≤ c
hc : C ≤ c ^ n
⊢ f =O[l] g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x ↦ ‖c‖ * ‖f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖c‖ * ‖f' x‖) ↔ f =O[l] f'

Tactic:
isBigO_const_mul_right_iff cne0,

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖f' x‖) ↔ f =O[l] f'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l f' g'
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
exact ((h₁ (div_pos cpos c'pos)).smul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

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 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) = ε
⊢ max N M + 1 < max N M + 1 + (max N M + 1)

Tactic:
exact lt_add_of_pos_left _ (Nat.succ_pos _)

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

Goal state before:
pp: x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)

Tactic:
refine sum_congr rfl fun n _ => ?_

Goal state after:
x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑n.factorial = (starRingEnd ℂ) (x ^ n / ↑n.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 - 1 + cos x ^ 2 = 2 * cos x ^ 2 - 1

Tactic:
sub_add_eq_add_sub,

Goal state after:
x : ℂ
⊢ cos x ^ 2 + cos x ^ 2 - 1 = 2 * cos x ^ 2 - 1
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
by
  rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
  simp_rw [← sub_eq_add_neg]
  calc ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
  _ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

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

Goal state before:
pp: x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = (cexp ↑x).re + (cexp (-↑x)).re

Tactic:
Complex.cosh,

Goal state after:
x : ℝ
⊢ ((cexp ↑x + cexp (-↑x)) / 2).re * 2 = (cexp ↑x).re + (cexp (-↑x)).re
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
by
  rw [← ofReal_inj]; simp [sinh_two_mul]

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (↑x * I)‖₊ = 1

Tactic:
by
  rw [← nnnorm_norm, norm_exp_ofReal_mul_I, ← NNReal.coe_eq_one]; simp

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

Goal state before:
pp: case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x

Tactic:
have hx' : 0 < x + 1 := by linarith

Goal state after:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖

Tactic:
by
      congr
      rw [exp_add]
      ring

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

Goal state before:
pp: ⊢ Tendsto rexp atTop atTop

Tactic:
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop :=
    tendsto_atTop_add_const_right atTop 1 tendsto_id

Goal state after:
A : Tendsto (fun x ↦ x + 1) atTop atTop
⊢ Tendsto rexp atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ 𝓝 0 = 𝓝 (-0)

Tactic:
neg_zero

Goal state after:
case e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ 𝓝 0 = 𝓝 0
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε

Tactic:
exact exists_congr fun _ ↦ and_comm

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'
n : ℕ
| r' ^ (n * k)

Tactic:
pow_mul

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'
n : ℕ
| (r' ^ n) ^ k
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
exact this.trans (le_of_eq (by ring))

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

Goal state before:
pp: case cons
M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
a✝¹ b✝ : M
l₁✝ l₂✝ : List M
h₁ : Joined a✝¹ b✝
a✝ : List.Forall₂ Joined l₁✝ l₂✝
h₂ : Joined l₁✝.prod l₂✝.prod
⊢ Joined (a✝¹ :: l₁✝).prod (b✝ :: l₂✝).prod

Tactic:
| cons h₁ _ h₂ =>

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

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ |p| * ‖↑(p⁻¹ * x)‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
inv_mul_cancel₀ hp,

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ |p| * ‖↑(p⁻¹ * x)‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x)) * (p⁻¹ * p)| ≤ |p⁻¹ * p| / 2

Tactic:
inv_mul_cancel₀ hp,

Goal state after:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x)) * 1| ≤ |1| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round (p⁻¹ * p / 2)) * p| = |p| / 2

Tactic:
inv_mul_cancel₀ hp,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round (1 / 2)) * p| = |p| / 2
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
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ (⇑γ ∘ f) 1 = y

Tactic:
simp [hf₁]

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - f (2 * n + 1) + f (2 * n + 1 + 1)

Tactic:
sub_add_eq_add_sub,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1 + 1) - f (2 * n + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x - f (2 * n + 1) + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
sub_add_eq_add_sub,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + f (2 * n + 2) - f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos √(1 - x ^ 2)

Tactic:
rw [eq_comm, ← cos_arcsin]

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
⊢ rexp 1 * x ≤ rexp x

Tactic:
← exp_le_exp,

Goal state after:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp (log x + 1) ≤ rexp (rexp (log x))
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
h : z.arg < 0
⊢ Real.sin z.arg < 0

Tactic:
exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

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

Goal state before:
pp: x y : ℝ
h : 0 < x
h₁ : 0 < y
⊢ log x ≤ log y ↔ x ≤ y

Tactic:
← exp_le_exp,

Goal state after:
x y : ℝ
h : 0 < x
h₁ : 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_le_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_le_exp,

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

Goal state before:
pp: x : ℂ
⊢ ↑x.re + (↑x.im - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π))) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
sub_mul,

Goal state after:
x : ℂ
⊢ ↑x.re + (↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I) =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
log_mul_ofReal,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ ↑(Real.log (normSq x)⁻¹) + log ((starRingEnd ℂ) x) = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
y : ℂ
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · rcases eq_or_ne y 0 with rfl | hy <;> simp [*, zero_zpow]
  · rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ + ↑(π / 2) - ↑ψ = 0
⊢ ↑θ + ↑ψ = ↑π

Tactic:
sub_add_eq_add_sub,

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) + ↑(π / 2) - ↑θ - ↑ψ = 0
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ - π + ψ = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
sub_add_eq_add_sub,

Goal state after:
θ ψ : ℝ
k : ℤ
H : θ + ψ - π = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ

Tactic:
rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]

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

Goal state before:
pp: θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ

Tactic:
by
  rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc; · exact hc
  rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs; · exact hs
  rw [eq_neg_iff_add_eq_zero, hs] at hc
  obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)
  rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
    eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one,
    ← Int.cast_ofNat, ← Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn
  have : (n * 2 + 1) % (2 : ℤ) = 0 % (2 : ℤ) := congr_arg (· % (2 : ℤ)) hn
  rw [add_comm, Int.add_mul_emod_self_right] at this
  exact absurd this one_ne_zero

Goal state after: