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
b₁ : β
⊢ ∀ (b : β), b₁ ≈ b → ∑' (a : α), f (a • b₁) = ∑' (a : α), f (a • b)

Tactic:
b₂

Goal state after:
α : 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
b₁ b₂ : β
⊢ b₁ ≈ b₂ → ∑' (a : α), f (a • b₁) = ∑' (a : α), f (a • b₂)
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : 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 α β) := ⋯
a : α
⊢ (orbitRel α β) (a • b) b

Tactic:
use a

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
⊢ Quotient.lift (fun b ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun b ↦ ∑' (a : α), f (a • b)) ⋯ (π b)

Tactic:
change ∑' a : α, g (π (a • b)) • f (a • b) = g (π b) • ∑' a : α, f (a • b)

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 (π (a • b)) • f (a • b) = g (π b) • ∑' (a : α), f (a • b)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ?m.43

Tactic:
congrm (ℑ ($((re_add_im z).symm) • a))

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = n • ‖x‖₊

Tactic:
by simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : PartialEquiv X Y
hc : ContinuousOn (↑e) e.source
ho : IsOpenMap (e.source.domRestrict ↑e)
hs : IsOpen[inst✝⁵] e.source
⊢ IsOpen[inst✝³] (PartialHomeomorph.ofContinuousOpenRestrict e hc ho).target

Tactic:
simpa [e.image_source_eq_target] using ho.isOpen_range

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

Goal state before:
pp: ⊢ Int.cast =Θ[cofinite] Int.cast

Tactic:
apply Asymptotics.IsTheta.of_norm_eventuallyEq_norm
  filter_upwards with n using by simp

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

Goal state before:
pp: ⊢ (exp' 0).lim = 1

Tactic:
refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩

Goal state after:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x ↦ ‖x‖) 1) j‖ < ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
x : α
⊢ ‖g x / g x‖ ≤ ‖1‖

Tactic:
simp [div_self_le_one]

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

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

Tactic:
grind [cos_two_mul, sin_sq_add_cos_sq]

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

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

Tactic:
simp [sin_sq_add_cos_sq]

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

Goal state before:
pp: x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

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

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

Tactic:
div_self two_ne_zero

Goal state after:
⊢ 1 ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin π = 0

Tactic:
rw [← mul_div_cancel_left₀ π two_ne_zero, two_mul, add_div, sin_add, cos_pi_div_two]

Goal state after:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0
Module: Mathlib.Analysis.Normed.Group.Quotient

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

Tactic:
mem_image

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (range cos).Infinite

Tactic:
rw [Real.range_cos]
  exact Icc_infinite (by simp)

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

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖

Tactic:
rw [mul_right_comm]

Goal state after:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this

Goal state after:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n ↦ ↑n ^ k) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n
⊢ (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

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

Tactic:
← div_le_one hεδ

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z / (ε + δ) ≤ 1
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
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 < δ
x : E
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← thickening_singleton, cthickening_thickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ.le)]

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖

Tactic:
by
  simp [dist_eq_norm', sum_range_succ]

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

Goal state before:
pp: M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
h : List.Forall₂ Joined l l'
⊢ Joined l.prod l'.prod

Tactic:
induction h with
  | nil => rfl
  | cons h₁ _ h₂ => exact h₁.mul h₂

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous[_, inst✝] ({1}.piecewise (const (↑I) y) (const (↑I) x))

Tactic:
exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h

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

Goal state before:
pp: x : ℝ
⊢ ‖↑x‖ = |x|

Tactic:
suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
    simp [norm_eq_infDist, this]
  ext y
  simp [eq_iff_sub_mem, sub_eq_zero]

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

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

Tactic:
show 2 * (n + 1) = 2 * n + 1 + 1 by ring,

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

Tactic:
show 2 * (n + 1) = 2 * n + 1 + 1 by ring,

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ γ.extend (if (if t₀ ≤ ↑1 then ↑1 else t₀) ≤ t₁ then if t₀ ≤ ↑1 then ↑1 else t₀ else t₁) = γ.extend t₁

Tactic:
split_ifs with h₁ h₂ 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₀ ≤ ↑1
h₂ : ↑1 ≤ t₁
⊢ γ.extend ↑1 = γ.extend t₁

case neg
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₀ ≤ ↑1
h₂ : ¬↑1 ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

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₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

case neg
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₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
Module: Mathlib.Topology.Path

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend (min t₀ t₁)

Tactic:
min_eq_left h

Goal state after:
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₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₀
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) ^ i * f i

Tactic:
show 2 * (n + 1) = 2 * n + 1 + 1 by ring,

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

Tactic:
show 2 * (n + 1) = 2 * n + 1 + 1 by ring,

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ Real.cos x.arg = x.re / ‖x‖

Tactic:
rw [arg]

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (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‖) - π) =
    x.re / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x; swap
  · rw [not_le] at hx₁
    rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
    nlinarith
  by_cases hx₂ : x ≤ 1; swap
  · rw [not_le] at hx₂
    rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
    nlinarith
  have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
  rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
    sqrt_mul_self (cos_arcsin_nonneg _)] at this
  rw [this, sin_arcsin hx₁ hx₂]

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = (↑y * I).arg

Tactic:
ofReal_mul',

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := y * I.re, im := y * I.im }.arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
abs_of_neg hx,

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

Goal state before:
pp: x : ℂ
⊢ log ((starRingEnd ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ) (log x)

Tactic:
by
  simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]
  split_ifs with hx
  · rw [hx]
  simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]

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

Goal state before:
pp: θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
coe_nsmul,

Goal state after:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = 2 • ↑(π / 2) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
simp only [him.not_ge]

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ -π / ↑n < θ.toReal ∧ θ.toReal ≤ π / ↑n

Tactic:
div_lt_iff₀' h',

Goal state after:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ -π < ↑n * θ.toReal ∧ θ.toReal ≤ π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: n : ℕ
z : ℂ
H : ↑n + 1 = 0 ∧ z ≠ 0
⊢ False

Tactic:
norm_cast at H; exact H.1

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

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

pp: case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg

Tactic:
· by_cases n0 : n = 0 <;> simp [n0]

Goal state after:
case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

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

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

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

Tactic:
by
  rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
  grind [sin_nonneg_of_nonneg_of_le_pi, sin_neg_of_neg_of_neg_pi_lt, toReal_mem_Ioc]

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

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y

Tactic:
rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg]

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

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
abs_of_neg hx,

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ (-x) ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain (h | h) : (θ + ψ).toReal ≤ 0 ∨ θ + ψ = π := by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

Goal state after:
case inl
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

case inr
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
by
  rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs
  have : ((θ + ψ).toReal : Angle) = ↑(θ.toReal + ψ.toReal) := by simp
  obtain ⟨k, hk⟩ := angle_eq_iff_two_pi_dvd_sub.mp this
  obtain (h | h) : (θ + ψ).toReal ≤ 0 ∨ θ + ψ = π := by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]
  · obtain rfl : k = -1 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos <| by
      grind [toReal_mem_Ioc]
    grind [abs_of_nonpos]
  · simp_all only [sign_coe_pi, ne_eq, zero_ne_one, not_false_eq_true, toReal_pi, coe_add,
      coe_toReal, pi_pos, abs_of_pos]
    obtain rfl : k = 0 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos (by grind)
    grind

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

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

Tactic:
rw [le_iff_eq_or_lt] at hx; rcases hx with hx | hx
  · rw [← hx, zero_rpow (ne_of_gt hz)]
    exact rpow_pos_of_pos (by rwa [← hx] at hxy) _
  · rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
    exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝

Tactic:
change ite _ _ _ = _

Goal state after:
case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 1 < 0 then ∞ else ↑(x✝ ^ 1)) = ↑x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : x ≤ 0
⊢ x < y ^ z

pp: case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
· exact hx.trans_lt (rpow_pos_of_pos hy _)

Goal state after:
case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
⊢ 1 ≤ x ^ z

Tactic:
cases x
  · simp [top_rpow_of_pos hz]
  · simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_le_rpow hx (le_of_lt hz)]

Goal state after:
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 x) x = y ↔ x = y

Tactic:
pointReflection_self

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
⊢ x = y ↔ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y = ⅟2 • (x + y)

Tactic:
by
  rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)

Tactic:
by
  rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]

Goal state after: