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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
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
⊢ Quotient (orbitRel α β) → M

Tactic:
by
  refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_
  intro b₁ b₂ ⟨a, (ha : a • b₂ = b₁)⟩
  rw [← ha]
  convert! (Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂)) using 1
  simp only [Equiv.coe_mulRight]
  congr
  ext
  congr 1
  simp only [mul_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| ↑(re z) + ↑0 * I

Tactic:
ofReal_zero,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| ↑(re z) + 0 * I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI').range = ℝ[I']

Tactic:
by
  simp_rw [← Algebra.map_top, ← adjoin_I, AlgHom.map_adjoin, Set.image_singleton, liftAux_apply_I]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
tfae_1_to_5 : (starRingEnd K) z = z → IsSelfAdjoint z
hz : IsSelfAdjoint z
⊢ (starRingEnd K) z = z

Tactic:
rwa [isSelfAdjoint_iff] at hz

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

Goal state before:
pp: ⊢ Metric.ball 1 1 ⊆ slitPlane

Tactic:
intro z hz
  apply Or.inl
  simpa using (re_le_norm _).trans_lt (mem_ball_iff_norm'.1 hz)

Goal state after:
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
⊢ star x * x = 1 ∧ x * star x = 1 ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun ⟨hx, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
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✝ : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
⊢ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

case refine_2
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✝ : IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
hx : IsStarNormal x
h : ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
⊢ star x * x = 1 ∧ x * star x = 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x

Tactic:
rwa [nhdsWithin_univ]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed ({a | re a.1 ≤ re a.2} ∩ {a | im a.1 = im a.2})

Tactic:
refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> fun_prop

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

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

pp: case calc_2
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ (n + i) / (↑n.factorial * ↑n.succ ^ i) =
    ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i)

pp: case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i) ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
· gcongr
    exact mod_cast Nat.factorial_mul_pow_le_factorial

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

case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i) ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E : Type u_3
E'' : Type u_9
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup E''
f : ℕ → E
g'' : ℕ → E''
h : f =O[atTop] g''
⊢ f =O[cofinite] g''

Tactic:
by rwa [Nat.cofinite_eq_atTop]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial) = ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / ↑m.factorial

Tactic:
by
      simp [← mul_sum, sum_Ico_eq_sum_range]

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

Goal state before:
pp: x : ℝ
⊢ ↑(cos (2 * x)) = ↑(1 - 2 * sin x ^ 2)

Tactic:
by simp [cos_two_mul_eq_one_sub]

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

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

Tactic:
by simp [sin_two_mul]

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

Goal state before:
pp: x : ℝ
this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
simp_all [add_comm, norm_def, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]

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

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

Tactic:
rw [exp_mul_I, norm_cos_add_sin_mul_I]

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑(x / 2) * I)) * (cexp (↑0 * I) - cexp (↑(x / 2 + x / 2) * I)) * I‖

Tactic:
ofReal_zero,

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑(x / 2) * I)) * (cexp (0 * I) - cexp (↑(x / 2 + x / 2) * I)) * I‖
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := ⋯
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
rw [← prod_atTop_atTop_eq]

Goal state after:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))
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
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ IsCauSeq abs fun m ↦ (1 - abv x ^ m) / (1 - abv x)

Tactic:
refine of_mono_bounded _ (a := (1 : α) / (1 - abv x)) (m := 0) ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ π / 2 ≤ 2

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]
  exact (Classical.choose_spec exists_cos_eq_zero).1.2

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

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
⊢ Summable fun i ↦ rexp (c * f i)

Tactic:
refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_
  refine Real.exp_monotone ?_
  conv_rhs => rw [mul_comm]
  exact mul_le_mul_of_nonpos_left (hf i) hc.le

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

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
| inl h =>

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

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬‖f‖ * ‖x‖ < ‖(lift S f.toAddMonoidHom hf) x‖

Tactic:
← lt_div_iff₀' h,

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬‖x‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
· have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
    rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this

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

Goal state before:
pp: case succ
R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
n✝ n : ℕ
hn : 1 ≤ n
IH : ‖x ^ n‖ = ‖x‖ ^ n
⊢ ‖x ^ (n + 1)‖ = ‖x‖ ^ (n + 1)

Tactic:
| succ n hn IH =>

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

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

Tactic:
have : 4 * (c * c) + (-2) * c + (-1) = 0 := by
    rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
    exact quadratic_root_cos_pi_div_five

Goal state after:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ c = (1 + √5) / 4
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 < ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z < ε

Tactic:
by
  refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ)
    (div_nonneg hδ <| add_nonneg hε.le hδ) <| by
      rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']).imp
    fun y hy => ?_
  rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
  rw [← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)] at h
  exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
⊢ (Summable fun n ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
⊢ ‖ξ‖ < 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1

Tactic:
simp only [norm_pow, dist_zero_right] at hk

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (↑π / 2) + sin (↑π / 2) * I = I

Tactic:
cos_pi_div_two,

Goal state after:
⊢ 0 + sin (↑π / 2) * I = I
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (↑π / 2) + sin (-(↑π / 2)) * I = -I

Tactic:
cos_pi_div_two,

Goal state after:
⊢ 0 + sin (-(↑π / 2)) * I = -I
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.closedBall b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall hε hδ]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ c • closedBall 0 1 = closedBall 0 ‖c‖

Tactic:
by
  rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]

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

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ = x * (1 - x)⁻¹ʳ ^ 2

Tactic:
calc (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ
    _ = (1 - x)⁻¹ʳ ^ 2 - ((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ := by
      simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
    _ = x * (1 - x)⁻¹ʳ ^ 2 := by noncomm_ring

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
push Not at H

Goal state after:
case neg
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
← mul_le_mul_iff_right₀ (abs_pos.mpr (inv_ne_zero hp)),

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

Goal state before:
pp: x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ |0| / 2 ≤ ε

Tactic:
simp [hε]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ cos (π / 2) = √(1 - x ^ 2)

Tactic:
cos_pi_div_two,

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ 0 = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (π / 2) = √(1 - x ^ 2)

Tactic:
cos_pi_div_two,

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 0 = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ

Tactic:
exact hcos.not_ge

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

Goal state before:
pp: case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ

Tactic:
exact hcos.not_ge

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

Goal state before:
pp: x : ℝ
⊢ log (-x) = log |x|

Tactic:
← log_abs (-x),

Goal state after:
x : ℝ
⊢ log |(-x)| = log |x|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

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

pp: case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0

Tactic:
Real.log_inv,

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: case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r

Tactic:
ofReal_zero,

Goal state after:
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (0 * ↑b) ^ r = 0 ^ r * ↑b ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r

Tactic:
ofReal_zero,

Goal state after:
case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * 0) ^ r = ↑a ^ r * 0 ^ r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h
  exact abs_sin_eq_of_two_nsmul_eq h

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

Goal state before:
pp: θ : Angle
⊢ (θ + ↑π).sign = -θ.sign

Tactic:
rw [sign, sign, sin_add_pi, Left.sign_neg]

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0

Tactic:
rw [← log_neg_eq_log, log_neg_iff (by linarith)]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑0 * I + ↑π * I) * y)

Tactic:
ofReal_zero,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + 0 * I + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
· simp [h rfl hw]

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

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
exact Real.rpow_sub_natCast (mod_cast hx) _ _

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

Goal state before:
pp: case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 ^ z < y ^ z

Tactic:
zero_rpow (ne_of_gt hz)

Goal state after:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun x ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
| inl h =>

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Tactic:
rw [← rpow_le_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne]

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
by
  rw [← rpow_lt_rpow_iff_of_neg _ hx hz, rpow_inv_rpow _ hz.ne] <;> positivity

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

Goal state before:
pp: case top
y : ℝ
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_left_inj hx _ hz, rpow_inv_rpow hy hz]; positivity

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

Goal state before:
pp: case insert
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, ↑(f i) ^ r = ↑(∏ i ∈ s✝, f i) ^ r
⊢ ↑(f a✝) ^ r * ↑(∏ i ∈ s✝, f i) ^ r = ↑(f a✝ * ∏ i ∈ s✝, f i) ^ r

Tactic:
← coe_mul_rpow,

Goal state after:
case insert
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, ↑(f i) ^ r = ↑(∏ i ∈ s✝, f i) ^ r
⊢ (↑(f a✝) * ↑(∏ i ∈ s✝, f i)) ^ r = ↑(f a✝ * ∏ i ∈ s✝, f i) ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
hb : 1 ≤ 1
⊢ Monotone fun x ↦ 1 ^ x

Tactic:
case inr => intro _ _ _; simp

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

Goal state before:
pp: case inr
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x ↦ 1 ^ x

Tactic:
case inr => intro _ _ _; simp

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

Goal state before:
pp: case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ 0 = rexp (log x * (1 / 2)) * cos (π / 2)

Tactic:
cos_pi_div_two,

Goal state after:
case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ 0 = rexp (log x * (1 / 2)) * 0
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection R (midpoint R x y)) y = x

Tactic:
midpoint_comm,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection R (midpoint R y x)) y = x
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection (midpoint R x y)) y = x

Tactic:
midpoint_comm,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection (midpoint R y x)) y = x