mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
pn.out,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range ↑nn = Finset.cons n' (Finset.range n') ⋯
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
have h₂ :
    (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k := by
    simp [Finset.mul_sum]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
⊢ abv ((∑ k ∈ range K, f k) * ∑ k ∈ range K, g k - ∑ n ∈ range K, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
← h₂,

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑(m.choose I * I.factorial * (m - I).factorial))⁻¹ =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v

Tactic:
rintro ⟨φ, hφ, h⟩
    exact isBigOWith_of_eq_mul φ hφ h

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
← lim_neg,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(exp' x).lim + (-const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖(exp' x).lim + -(const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
← lim_neg,

Goal state after:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖(exp' x).lim + (-const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos (x + y)) = ↑(cos x * cos y - sin x * sin y)

Tactic:
simp [cos_add]

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

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

Tactic:
by simp [cos_two_mul']

Goal state after:
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
⊢ HasSum (fun x ↦ f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)

Tactic:
let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2

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
⊢ HasSum (fun x ↦ f x.1 * g x.2) ((∑' (i : ι), f i) * ∑' (j : ι'), g j)
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d

Tactic:
simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d

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

Goal state before:
pp: ⊢ Function.Antiperiodic cos π

Tactic:
simp [cos_add]

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

Goal state before:
pp: x : ℝ
⊢ cos (x + π / 2) = -sin x

Tactic:
simp [cos_add]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) (Neg.neg '' ↑S) = ⨅ a, ‖m + ↑a‖

Tactic:
image_neg_eq_neg,

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) (-↑S) = ⨅ a, ‖m + ↑a‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 0 ≤ 2

case hx
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π

Tactic:
exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = θ

Tactic:
hθ

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = π / 5
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_mul_comm,

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 ≤ ε + δ
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
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ δ / (ε + δ) * dist x z ≤ δ ∧ ε / (ε + δ) * dist x z < ε

Tactic:
div_mul_comm,

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

Tactic:
div_mul_comm,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ ε / (ε + δ) * dist x z < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ - -2 - 2 * √5 < 0

Tactic:
by norm_num [lt_sqrt]

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

Goal state before:
pp: ⊢ Function.Antiperiodic cos ↑π

Tactic:
simp [cos_add]

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

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

Tactic:
simp [cos_add]

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

Tactic:
intro h'
    rw [pathComponent_symm]
    exact (h.trans h').symm

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range ⇑γ.extend

Tactic:
intro x _hx

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ (γ.truncate t₀ t₁) ⟨x, _hx⟩ ∈ range ⇑γ.extend
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
key : Continuous fun x ↦ (t, x)
⊢ Continuous[_, inst✝] ↿(γ.truncate t)

Tactic:
exact γ.truncate_continuous_family.comp key

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

Goal state before:
pp: case inr.inr.inl.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ False

Tactic:
have : p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]

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

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

Tactic:
sqrt_eq_zero_of_nonpos

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ 0 = 0

case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
· 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

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
sqrt_eq_zero_of_nonpos

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 0 = 0

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ (x / √(1 - x ^ 2))⁻¹ = √(1 - x ^ 2) / x

Tactic:
inv_div

Goal state after:
x : ℝ
⊢ √(1 - x ^ 2) / x = √(1 - x ^ 2) / x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ ↑(expOrderIso (expOrderIso.symm ⟨|x|, ⋯⟩)) = |x|

Tactic:
OrderIso.apply_symm_apply,

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ ↑⟨|x|, ⋯⟩ = |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
rw [exp_log_eq_abs h_zero]
    exact le_abs_self _

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

Goal state before:
pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
· convert! toIocMod_mem_Ioc ..
    ring

Goal state after:
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 = -(π / 2)

Tactic:
· obtain ⟨x, y⟩ := z
    rintro ⟨rfl : x = 0, hy : y < 0⟩
    rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]
    simp

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log √x = log x / 2

Tactic:
rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]
  exact two_ne_zero

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

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (s ∩ range cexp)

Tactic:
range_exp,

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (s ∩ {0}ᶜ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0

Tactic:
range_exp,

Goal state after:
⊢ 𝓝 0 ⊓ 𝓟 {0}ᶜ = 𝓝[≠] 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ cobounded ℂ ⊓ 𝓟 (range cexp) = cobounded ℂ

Tactic:
range_exp,

Goal state after:
⊢ cobounded ℂ ⊓ 𝓟 {0}ᶜ = cobounded ℂ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ x ^ 1 = x

pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
cpow_one

Goal state after:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ x = x

x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]

Goal state after:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x ^ 1 = x

pp: case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

pp: case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π

Tactic:
cpow_one

Goal state after:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x = x

case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]
    simp [hre.ne, hre.not_ge, hre.not_gt, this]

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

Goal state before:
pp: θ : Angle
⊢ (θ - ↑(π / 2)).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on
  exact Real.cos_sub_pi_div_two _

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

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

Tactic:
rw [two_nsmul_eq_iff] at h
  rcases h with (rfl | rfl)
  · rfl
  · rw [cos_add_pi, abs_neg]

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

Goal state before:
pp: θ : Angle
⊢ |θ.toReal| = π / 2 ↔ θ.cos = 0

Tactic:
abs_toReal_eq_pi_div_two_iff,

Goal state after:
θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = ↑(-π / 2) ↔ θ.cos = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
have h_rpow_nonneg : 0 ≤ x ^ y := Real.rpow_nonneg hx_nonneg _

Goal state after:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: b : ℂ
hb : b ≠ 0
⊢ (fun x ↦ 0 ^ x) =ᶠ[𝓝 b] 0

Tactic:
suffices ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [zero_cpow hx, Pi.zero_apply]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ log (x ^ y) = y * log x

Tactic:
apply exp_injective
  rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]

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

Goal state before:
pp: y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).1 ^ (0, a).2 = 0

Tactic:
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'

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

Goal state before:
pp: x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← NNReal.coe_inj, coe_rpow, NNReal.coe_pow]

Goal state after:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ n) ^ (↑n)⁻¹ = ↑x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

Tactic:
rcases hy.eq_or_lt with rfl | hy

Goal state after:
case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z

case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z
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

Tactic:
exact hx.trans (rpow_pos_of_pos hy _).le

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

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0

Tactic:
linarith only [hs]

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

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0

Tactic:
linarith only [hs]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₃ • r₂ • y = r₂ • r₄ • z

Tactic:
← h₂,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₃ • r₂ • y = r₂ • r₃ • y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

Tactic:
simp [lineMap_apply_module', smul_sub, sub_smul]; abel

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
⊢ (lineMap p₀ p₁) y ≤ (lineMap p₀ p₁) x

Tactic:
suffices y • (p₁ - p₀) ≤ x • (p₁ - p₀) by simpa [lineMap]

Goal state after:
k : Type u_1
V1 : Type u_2
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : LinearOrder k
inst✝² : Preorder V1
inst✝¹ : AddLeftMono V1
inst✝ : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
⊢ y • (p₁ - p₀) ≤ x • (p₁ - p₀)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_1
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1

Tactic:
rw [← add_div, add_comm, div_self h₁₂.ne']

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

Goal state before:
pp: case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
i : ι
x : φv i
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x) = f.linear (Pi.single i x) +ᵥ f 0
s₃ : g (Pi.single i x) = g.linear (Pi.single i x) +ᵥ g 0
h₂ : f (Pi.single i 0) = g (Pi.single i 0)
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)

Tactic:
simp only [Pi.single_zero] at h₂

Goal state after:
case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
i : ι
x : φv i
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x) = f.linear (Pi.single i x) +ᵥ f 0
s₃ : g (Pi.single i x) = g.linear (Pi.single i x) +ᵥ g 0
h₂ : f 0 = g 0
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
rintro _ ⟨y, hy, rfl⟩ a b ha hb hab
  exact ⟨a • x + b • y, hs hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) * x + (z - x) * y) / (y - x) = z

Tactic:
div_eq_iff h.ne',

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) * x + (z - x) * y = z * (y - x)