mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
toMulEquiv✝¹ : A ≃* B
map_star'✝¹ : ∀ (a : A), toMulEquiv✝¹.toFun (star a) = star (toMulEquiv✝¹.toFun a)
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h :
  { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.toFun =
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun
⊢ { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.invFun =
      { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun →
    { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ } = { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0

Tactic:
rw [← norm_eq_zero, norm_star_mul_self]

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
⊢ f.comp (ι f g) = g.comp (ι f g)

Tactic:
by
  ext x
  rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]
  exact x.2

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π (a • b)) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)

Tactic:
simp_rw [H₁]

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π b) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ ‖{ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
            invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
          x✝‖ ^
      2 =
    ‖x✝‖ ^ 2

Tactic:
← normSq_eq_norm_sq,

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ normSq
      ({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝) =
    ‖x✝‖ ^ 2
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
rw [← RCLike.ofReal_eq_complex_ofReal]
  exact RCLike.norm_of_nonneg' hx

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

Goal state before:
pp: z : ↥(selfAdjoint ℂ)
⊢ ↑(selfAdjointEquiv z) = ↑z

Tactic:
by
  simpa [selfAdjointEquiv_symm_apply]
    using (congr_arg Subtype.val <| Complex.selfAdjointEquiv.left_inv z)

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ 2 • I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
smul_eq_zero_iff_right two_ne_zero,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ * ‖I‖ = 1

Tactic:
← norm_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I * I‖ = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:

Tactic:
‖re x - re y‖ₑ
  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
x✝ : I = 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: f g : ℂ → ℂ
x : ℝ
h : f =O[𝓝[≠] ↑x] g
x✝¹ : ℝ
x✝ : x✝¹ ∈ {x}ᶜ
⊢ ↑x✝¹ ∈ {↑x}ᶜ

Tactic:
simp_all

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

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 α
inst✝ : Subsingleton E'
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖g' x‖

Tactic:
by simp [Subsingleton.elim (f' _) 0, mul_nonneg hc.le]

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

Goal state before:
pp: n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ IsNat (n.ascFactorial l) a

Tactic:
constructor
  simp [h₁.out, h₂.out, ← p]

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

Goal state before:
pp: x y : ℂ
⊢ (cexp x - cexp (-x)) * (2 * cosh y) + 2 * (cosh x * (cexp y - cexp (-y))) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))

Tactic:
two_cosh,

Goal state after:
x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + 2 * (cosh x * (cexp y - cexp (-y))) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ 2 * cosh (x + y) = 2 * (cosh x * cosh y + sinh x * sinh y)

Tactic:
two_cosh,

Goal state after:
x y : ℂ
⊢ cexp (x + y) + cexp (-(x + y)) = 2 * (cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ 2 * cosh x * cosh y + 2 * (sinh x * sinh y) = cexp x * cexp y + cexp (-x) * cexp (-y)

Tactic:
two_cosh,

Goal state after:
x y : ℂ
⊢ (cexp x + cexp (-x)) * cosh y + 2 * (sinh x * sinh y) = cexp x * cexp y + cexp (-x) * cexp (-y)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ (cexp x + cexp (-x)) * (2 * cosh y) + 2 * ((cexp x - cexp (-x)) * sinh y) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))

Tactic:
two_cosh,

Goal state after:
x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + 2 * ((cexp x - cexp (-x)) * sinh y) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h : ↑(cexp ↑x).re = ↑0
⊢ cexp ↑x = 0

Tactic:
simp_all

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (cauSeqRe (exp' ↑x)).lim = (exp' ↑x).lim.re

Tactic:
lim_re

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (exp' ↑x).lim.re = (exp' ↑x).lim.re
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
two_cosh,

Goal state after:
x : ℂ
⊢ cexp x + cexp (-x) + 2 * sinh x = 2 * cexp x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ 2 * cosh x - 2 * sinh x = 2 * cexp (-x)

Tactic:
two_cosh,

Goal state after:
x : ℂ
⊢ cexp x + cexp (-x) - 2 * sinh x = 2 * cexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
two_cosh,

Goal state after:
x : ℂ
⊢ cexp (x * I) + cexp (-(x * I)) = 2 * cos x
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) = ε
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
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n) < ε

Tactic:
h₂,

Goal state after:
α : 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
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k) < ε
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
sinh_eq,

Goal state after:
x : ℝ
⊢ (rexp x - rexp (-x)) / 2 / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 5 / 100

Tactic:
by
  simpa [← ofReal_sin, ← norm_eq_abs, ← norm_real] using Complex.sin_bound (x := x) (by simpa)

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ≤ 1

Tactic:
by rwa [abs_of_nonneg (le_of_lt hx0)]

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

Goal state before:
pp: case ha
⊢ 0 ≤ cos 1

pp: case hab
⊢ cos 1 ≤ 5 / 9

Tactic:
· exact cos_one_pos.le

Goal state after:
case hab
⊢ cos 1 ≤ 5 / 9
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp ↑⌈x⌉₊ / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * C)

Tactic:
by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x) '' {m | ↑m = ↑x}) = infDist x ↑S

Tactic:
← IsometryEquiv.preimage_symm

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist ((IsometryEquiv.divLeft x) 1) (⇑(IsometryEquiv.divLeft x).symm ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s * t)

Tactic:
by
  obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
  obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
  refine isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, ?_⟩
  rintro z ⟨x, hx, y, hy, rfl⟩
  exact norm_mul_le_of_le' (hRs x hx) (hRt y hy)

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

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

Tactic:
rw [singleton_div_sphere, div_one]

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

Goal state before:
pp: case e'_2
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

pp: case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ

Tactic:
· exact s.biUnion_of_singleton.symm

Goal state after:
case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ SurjOn cos (Icc 0 π) (Icc (-1) 1)

Tactic:
by
  simpa only [cos_zero, cos_pi] using! intermediate_value_Icc' pi_pos.le continuous_cos.continuousOn

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
    simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]

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

Goal state before:
pp: ⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto using 2

Goal state after:
case e'_5
⊢ -1 = sin (-(π / 2))
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
· intro y y_in
    rwa [← h] at y_in

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

Goal state before:
pp: f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
simp_rw [mul_comm]

Goal state after:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, f x * (-1) ^ x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
simp_rw [mul_comm]

Goal state after:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, f x * (-1) ^ x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = ↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm) x)

Tactic:
IccExtend,

Goal state after:
x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = ↑((⇑sinOrderIso.symm ∘ projIcc (-1) 1 arcsin._proof_2) x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ sinh (log x) = (x - x⁻¹) / 2

Tactic:
sinh_eq,

Goal state after:
x : ℝ
hx : 0 < x
⊢ (rexp (log x) - rexp (-log x)) / 2 = (x - x⁻¹) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < -x

Tactic:
neg_lt_neg_iff

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ ∀ x ∈ s.toList, x ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ ∀ x ∈ List.map (fun i ↦ f i) s.toList, x ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr.le, hr.le.not_gt]

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

Goal state before:
pp: case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr.le, hr.le.not_gt]

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

Goal state before:
pp: x : ℂ
⊢ |x⁻¹.arg| = |x.arg|

Tactic:
rw [arg_inv]; split_ifs <;> simp [*]

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

Goal state before:
pp: case mpr
θ : Angle
h : θ ≠ ↑π
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π

Tactic:
neg_lt_neg_iff

Goal state after:
case mpr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(x.arg - π) = ↑x.arg + ↑π

Tactic:
Real.Angle.coe_sub,

Goal state after:
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑x.arg - ↑π = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← sin_toReal,

Goal state after:
θ : Angle
⊢ θ.toReal < 0 ↔ SignType.sign (Real.sin θ.toReal) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = SignType.sign θ.sin

Tactic:
← sin_toReal,

Goal state after:
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = SignType.sign (Real.sin θ.toReal)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = rexp (log x * y)

Tactic:
if_neg (ne_of_gt hx)

Goal state after:
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log x * y) = rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (hs | hs) := hs
  · obtain (h | h | h) := ψ.sign.trichotomy <;> obtain (h | h | h) := θ.sign.trichotomy
    all_goals grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]
  · rw [← neg_neg θ.sign, ← sign_neg] at hs
    have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm
    simpa [toReal_neg_eq_neg_toReal_iff.mpr, hθ, ← sub_eq_add_neg, eq_sub_iff_add_eq', eq_comm]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
⊢ (have this := fun x ↦ ‖f x‖ ^ (g x).re / 1;
    this) =ᶠ[l]
    have this := fun x ↦ ‖f x‖ ^ (g x).re;
    this

Tactic:
by
      simp only [div_one, EventuallyEq.rfl]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl_im : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0
⊢ (fun x ↦ ‖f x‖ ^ (g x).re / 1) =ᶠ[l] fun x ↦ ‖f x‖ ^ (g x).re

Tactic:
by
      simp only [div_one, EventuallyEq.rfl]

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

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ (c * |g x|) ^ r = c ^ r * |g x ^ r|

Tactic:
rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

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

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

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : z = 0
⊢ 1 = x ^ z * y ^ z

Tactic:
simp_all

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

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : ¬z = 0
⊢ 0 = x ^ z * y ^ z

Tactic:
simp_all

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

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

Tactic:
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
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h✝ : z = 0
⊢ rexp (log (x * y) * z) = 1 * y ^ z

Tactic:
simp_all

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

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

Tactic:
simp_all

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

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

Tactic:
simp_all

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 = 0 x

Tactic:
Pi.zero_apply

Goal state after:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
⊢ (fun x ↦ x ^ b) =ᶠ[𝓝 a] fun x ↦ cexp (Complex.log x * b)

Tactic:
suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [cpow_def_of_ne_zero hx]
  exact IsOpen.eventually_mem isOpen_ne ha

Goal state after: