mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case pos
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
by_cases hL : L.NeBot

Goal state after:
case pos
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x

Tactic:
ext <;> simp [smul_re, smul_im, add_smul]

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

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

Tactic:
map_add,

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

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

Tactic:
← mul_assoc,

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ normSq ((starRingEnd K) z) = normSq z

Tactic:
simp only [normSq_apply, neg_mul, mul_neg, neg_neg, rclike_simps]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = 1

Tactic:
← mul_assoc,

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹ = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
· exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ a

Tactic:
← realPart_add_I_smul_imaginaryPart a,

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ ↑(ℜ a) + I • ↑(ℑ a)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ unitary A ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
Unitary.mem_iff

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x = 1 ∧ x * star x = 1 ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
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:
simp only [map_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y

Tactic:
by
      rw [RCLike.le_iff_re_im] at *
      simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x = { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
subst h''; exact h.smul_def'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun x ↦ f (x, y)) =Θ[l] fun x ↦ g (x, y)

Tactic:
by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

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 < ε
n : ℕ
hn : ε⁻¹ < ↑n
hn₀ : 0 < ↑n
x : α
hfg : ‖f x‖ ≤ (↑n)⁻¹ * ‖g x‖
⊢ 0 ≤ ‖g x‖

Tactic:
refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x

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
hn₀ : 0 < ↑n
x : α
hfg : ‖f x‖ ≤ (↑n)⁻¹ * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ 0 < (↑n)⁻¹
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g
⊢ IsBigOWith (∑ i ∈ Finset.cons i s is, C i) l (∑ i ∈ Finset.cons i s is, A i) g

Tactic:
simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢

Goal state after:
case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith (C i + ∑ i ∈ s, C i) l (A i + ∑ i ∈ s, A i) g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Tactic:
simp only [hc, false_or, isLittleO_const_left_of_ne hc]

Goal state after:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
c : E''
hc : c ≠ 0
⊢ Tendsto (fun x ↦ ‖g'' x‖) l atTop ↔ Tendsto (norm ∘ g'') l atTop
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: 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))

Tactic:
← mul_assoc,

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.Exponential

Goal state before:
pp: case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝

Tactic:
· simp [exp_add, add_mul, pow_add, exp_neg, exp_nat_mul]

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

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

Tactic:
← mul_assoc,

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 : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
by
  rw [two_mul, sinh_add]
  ring

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

Goal state before:
pp: x : ℂ
⊢ cexp (x * I) - cexp (-(x * I)) = 2 * (sin x * I)

Tactic:
← mul_assoc,

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|

Tactic:
have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Goal state after:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2

Tactic:
have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Goal state after:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by
  rw [exp_mul_I, norm_cos_add_sin_mul_I]

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

Goal state before:
pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Tactic:
simp only [expNear, mul_zero, add_zero]
  convert! exp_bound (n := m) h ?_ using 1
  · simp [field]
  · lia

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn <;> simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
by gcongr; apply norm_mul_le

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

Goal state before:
pp: x c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * rexp (c * x)

Tactic:
by
  rw [le_inv_mul_iff₀ hc]
  calc c * x
  _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
  _ ≤ _ := Real.add_one_le_exp (c * x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr hb

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

Goal state before:
pp: case inr
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
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
· convert! (H (-b) (-c) (neg_pos.mpr h)).neg using 1
    · ext x
      field_simp
      rw [← neg_add (b * exp x) c, div_neg, neg_neg]
    · rw [neg_zero]

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

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
← mul_assoc,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * 2 * π = x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f (m + x) = f m

Tactic:
map_add,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m + f x = f m
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = 2 * s * c

Tactic:
← mul_assoc,

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * 2 * c = 2 * s * c
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩

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

Goal state before:
pp: ⊢ cos (↑π / 2) = ↑(Real.cos (π / 2))

Tactic:
rw [ofReal_cos]; simp

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

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

Tactic:
Metric.vadd_ball,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

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

Tactic:
Metric.vadd_ball,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑n ^ k * r ^ n

Tactic:
refine Nat.strong_induction_on k fun k hk => ?_

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
⊢ Summable fun n ↦ ↑n ^ k * r ^ n
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_2
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
⊢ s ∈ 𝓝 (const X c)

Tactic:
filter_upwards [eventually_mapsTo hK isOpen_interior fun x _ ↦
      mem_interior_iff_mem_nhds.mpr <| h.mem_of_mem hpi] with f hf

Goal state after:
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
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin n), p i ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ

Tactic:
induction p using snocInduction generalizing x with
  | elim0 =>
    simp only [snoc_zero]
    use Path.refl x
    simp [hx]
  | @snoc n p y hp₂ =>
    simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
    obtain ⟨hp, hy⟩ := hp
    specialize hp₂ y hp hy
    obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
    obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
    rw [← range_subset_iff] at hγ₁
    use γ₀.trans γ₁
    simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]
    tauto

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

Goal state before:
pp: case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0

Tactic:
rw [round_eq_zero_iff]

Goal state after:
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₀

Tactic:
have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)

Goal state after:
case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄✝ : t₀ ≤ t₁
h₄ : t₁ ≤ 0
⊢ γ.extend t₁ = γ.extend t₀
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ ↑(addOrderOf u) * (p * (↑n / ↑(addOrderOf u)))

Tactic:
← mul_assoc,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ ↑(addOrderOf u) * p * (↑n / ↑(addOrderOf u))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ arccos x = y

Tactic:
rw [hxy, arccos_cos hy₀ hy₁]

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

Goal state before:
pp: x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| (↑r * (↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I))).arg

Tactic:
← mul_assoc,

Goal state after:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| (↑r * ↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I)).arg
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hf
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖)

Tactic:
change IsBoundedUnder _ _ fun _ ↦ _
    simpa using hbdd

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

Goal state before:
pp: z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [norm_nonneg]
  · obtain ⟨x, y⟩ := z
    rintro ⟨h, rfl : y = 0⟩
    exact arg_ofReal_of_nonneg h

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑x.re + ↑‖x‖ * (↑x.im / ↑‖x‖ * I) = x

Tactic:
← mul_assoc,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ ↑x.re + ↑‖x‖ * (↑x.im / ↑‖x‖) * I = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log (r * ‖x‖)) + ↑x.arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
Real.log_mul hr.ne' hx,

Goal state after:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log r + Real.log ‖x‖) + ↑x.arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
map_add,

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) ≤ log (1 + x)

Tactic:
by
  rw [le_log_iff_exp_le (by grind)]
  convert exp_le_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
  all_goals field_simp; grind

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

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

Tactic:
map_add,

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

Goal state before:
pp: ⊢ ContinuousOn log {0}ᶜ

Tactic:
by
  simp +unfoldPartialApp only [continuousOn_iff_continuous_domRestrict,
    domRestrict]
  conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
  exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

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

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
⊢ cexp (2 * ↑π * I * ↑k / ↑N) = 1 ↔ N ∣ k

Tactic:
rw [exp_eq_one_iff]
  conv in _ = _ => rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]
  field_simp [Nat.cast_ne_zero.mpr hN]
  norm_cast
  simp [← dvd_def, Int.ofNat_dvd]

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (𝓝 0)

Tactic:
← comap_exp_nhds_exp,

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (comap rexp (𝓝 (rexp 0)))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
by
  simp only [cpow_def, neg_eq_zero, mul_neg]
  split_ifs <;> simp [exp_neg]

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
· simp only [him]
    rw [iff_true, arg_of_re_neg_of_im_neg hre him]
    exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

Goal state after: