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

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
⊢ Continuous[inst✝ j, inst✝ i] (AlgEquiv.cast h).invFun

Tactic:
by cases h; exact continuous_id

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

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

Tactic:
rw [map_neg, conj_I, neg_neg]

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

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : ↑b = ∑ i ∈ s, ↑‖f i‖
⊢ a ≤ b

Tactic:
norm_cast at hb; rw [← Complex.norm_of_nonneg ha₀, ha, hb]; exact norm_sum_le s f

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ |2 * re x| ^ 2 = re ↑(2 * re x) ^ 2

Tactic:
sq_abs,

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ (2 * re x) ^ 2 = re ↑(2 * re x) ^ 2
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ 𝓝[e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s] ↑e x = 𝓝[s] ↑e x

Tactic:
e.target_inter_inv_preimage_preimage,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ 𝓝[e.target ∩ s] ↑e x = 𝓝[s] ↑e x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im x - im y‖ₑ = ‖im (x - y)‖ₑ

Tactic:
map_sub im x y

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im x - im y‖ₑ = ‖im x - im y‖ₑ
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
⊢ (starRingEnd 𝕜) I = -I

Tactic:
subst h''; exact h.conj_I_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
filter_upwards [hfg, hgk] with x hx hx'

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * c' * ‖k x‖
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:
by
  simp only [← principal_univ, isLittleO_principal, mem_univ, forall_true_left]

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ |‖z ^ m.succ / ↑m.succ.factorial‖| ≤ ‖z‖ / ↑n * |‖z ^ m / ↑m.factorial‖|

Tactic:
abs_norm,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z ^ m.succ / ↑m.succ.factorial‖ ≤ ‖z‖ / ↑n * |‖z ^ m / ↑m.factorial‖|
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z ^ m.succ / ↑m.succ.factorial‖ ≤ ‖z‖ / ↑n * |‖z ^ m / ↑m.factorial‖|

Tactic:
abs_norm,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z ^ m.succ / ↑m.succ.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
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₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
c' : ℝ
c'pos : c' > 0
hc' : IsBigOWith c' l k₁ k₂
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

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

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

Goal state before:
pp: case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
h₂ : ∃ i_1 ∈ i :: L, f i_1 =o[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢

Goal state after:
case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
h₂ : f i =o[l] g i ∨ ∃ x ∈ L, f x =o[l] g x
⊢ (fun x ↦ f i x * (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ g i x * (List.map (fun x_1 ↦ g x_1 x) L).prod
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ 1 = cexp x ^ 0

Tactic:
pow_zero

Goal state after:
x : ℂ
⊢ 1 = 1
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by
  rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : x ∈ {x | (fun x ↦ ‖f₁ x‖ ≤ c * ‖f₂ x‖) x}
⊢ x ∈ {x | (fun x ↦ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖) x}

Tactic:
simp only [mem_ofPred_eq] at hx ⊢
      rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]
      · exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)
      · exact sub_pos.2 hc

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

Goal state before:
pp: x : ℂ
⊢ sin ((2 + 1) * x) = (2 + 1) * sin x - 4 * sin x ^ 3

Tactic:
add_one_mul,

Goal state after:
x : ℂ
⊢ sin (2 * x + x) = (2 + 1) * sin x - 4 * sin x ^ 3
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos |x| = cos x

Tactic:
cases le_total x 0 <;> simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
have h' := Real.exp_bound h4 hn

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Trigonometric

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

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

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

Goal state before:
pp: n : ℕ
x r : ℝ
⊢ x ^ n * x * ((↑n.factorial)⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑n.factorial)⁻¹ * (x * (↑n + 1)⁻¹ * r)

Tactic:
ac_rfl

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

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

Tactic:
ac_rfl

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

Goal state before:
pp: α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑⟨rexp x, ⋯⟩) atTop atTop

Tactic:
simp only [tendsto_exp_atTop]

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

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

Tactic:
by
  simpa using cos_add_int_mul_pi 0 n

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

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ sin x = 1 ∨ sin x = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]

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

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

Tactic:
by
  trans sin (π / 2 ^ 3)
  · congr
    norm_num
  · 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
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' Ioo a b = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
← image_image (· * r),

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ x * r) '' norm '' Ioo a b = ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
simp only [← cast_pow]

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ‖↑(n ^ k) * r ^ n‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h2
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), cos x ∈ Ioi 0

Tactic:
filter_upwards [Ioo_mem_nhdsLT (neg_lt_self pi_div_two_pos)] with x hx
    exact cos_pos_of_mem_Ioo hx

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

Goal state before:
pp: z : ℂ
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]

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

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

Tactic:
obtain hδ | hδ := le_or_gt δ 0

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

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
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
⊢ Metric.ball a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)

Tactic:
ball_add_ball hε hδ

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

Goal state before:
pp: a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ ‖cexp (↑a * (cexp z + cexp (-z)))‖ ≤ rexp (a * Real.cos b * rexp |z.re|)

Tactic:
simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ←
    add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
  have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
    apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
  refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha
  · exact
      Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
        (hb.trans <| half_le_self <| Real.pi_pos.le) hz
  · refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩
    exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
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)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
⊢ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} ⊆
    {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U}

Tactic:
intro f

Goal state after:
case refine_1
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)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
⊢ f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} →
    f ∈ {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U}
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n

Tactic:
sum_range_succ,

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist (∑ i ∈ Finset.range n, f i) (∑ x ∈ Finset.range n, f x + f n) ≤ C * r ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ γ.extend (2 * ↑t) = γ ⟨2 * ↑t, ⋯⟩

Tactic:
extend_apply

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑t, ?pos.ht✝⟩ = γ ⟨2 * ↑t, ⋯⟩

case pos.ht
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ Icc 0 1
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ γ'.extend (2 * ↑t - 1) = γ' ⟨2 * ↑t - 1, ⋯⟩

Tactic:
extend_apply

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑t - 1, ?neg.ht✝⟩ = γ' ⟨2 * ↑t - 1, ⋯⟩

case neg.ht
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 2 * ↑t - 1 ∈ Icc 0 1
Module: Mathlib.Topology.Path

Goal state before:
pp: case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ γ₁ ⟨2 * ↑⟨t, ⋯⟩, ⋯⟩ = γ₁.extend (2 * t)

pp: case inr.hc
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ ↑⟨t, ⋯⟩ ≤ 1 / 2

Tactic:
extend_apply

Goal state after:
case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ γ₁ ⟨2 * ↑⟨t, ⋯⟩, ⋯⟩ = γ₁ ⟨2 * t, ?inr.ht⟩

case inr.ht
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ 2 * t ∈ Icc 0 1

case inr.hc
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ ↑⟨t, ⋯⟩ ≤ 1 / 2
Module: Mathlib.Topology.Instances.ZMultiples

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

Tactic:
rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))

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), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
sum_range_succ,

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 : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
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 : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1 + 1), (-1) ^ i * f i

Tactic:
sum_range_succ,

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 : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 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 : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1 + 1 + 1), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i

Tactic:
sum_range_succ,

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 + 2), (-1) ^ x * f x + (-1) ^ (2 * n + 2) * f (2 * n + 2) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = π / 2

Tactic:
projIcc_of_right_le _ hx,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ arcsin ↑⟨1, ⋯⟩ = π / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : 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‖
⊢ Tendsto (fun x ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)

Tactic:
apply isBoundedUnder_le_mul_tendsto_zero

Goal state after:
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‖)

case hg
α : 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‖
⊢ Tendsto (fun x ↦ ‖g x‖) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
obtain ⟨x, y⟩ := z
    rintro ⟨h : x < 0, rfl : y = 0⟩
    rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
    simp [← ofReal_def]

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

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

Tactic:
refine log_lt_log (abs_pos.2 hy.ne) ?_

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

Goal state before:
pp: s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ log s.prod = (Multiset.map (fun x ↦ log x) s).sum

Tactic:
by
  rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]

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

Goal state before:
pp: n : ℕ
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp -- relies on junk values of `log` and `Nat.factorization`
  · simp only [← log_pow, ← Nat.cast_pow]
    rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]
    intro p hp
    rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

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

Goal state before:
pp: x y : ℂ
⊢ cexp x = cexp y ↔ cexp x / cexp y = 1

Tactic:
div_eq_one_iff_eq (exp_ne_zero _)

Goal state after:
x y : ℂ
⊢ cexp x = cexp y ↔ cexp x = cexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Goal state after:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Goal state after:
case inl.inr.inl
n : ℤ
hn : n ≠ 0
⊢ 0 ^ (↑n * 0) = (0 ^ 0) ^ n

case inl.inr.inr
n : ℤ
y : ℂ
hn : n ≠ 0
hy : y ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n