mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))

Tactic:
refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_right)
    filter_upwards [self_mem_nhdsWithin] with y hy
    replace hy : x ≤ y := hy.le
    simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_le, hy, h]

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ↑C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ = (↑C + ‖L‖ + 1) * δ * ρ

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun y ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ (↑n !)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, (x - t) ^ n / ↑n ! * iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
rcases eq_or_ne x₀ x with rfl | this
  · simp
  apply taylor_integral_remainder_aux
  intro k hk
  apply AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul
  · apply ContDiffOn.absolutelyContinuousOnInterval
    fun_prop
  · rcases hk.eq_or_lt with rfl | hk
    · exact hf₂
    replace hf₁ := hf₁.of_le (m := k.succ) (by norm_cast)
    grind [ContDiffOn.absolutelyContinuousOnInterval, uniqueDiffOn_uIcc,
      contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin]

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

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + (s * x) ^ 2 = 1 - 2 * x + (1 + s ^ 2) * x * x

Tactic:
ring

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

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + (s * x) ^ 2 = (1 + s ^ 2) * x ^ 2

Tactic:
ring

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

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √((1 + s ^ 2) * x ^ 2) = √(1 + s ^ 2) * x

Tactic:
sqrt_mul' _ (sq_nonneg x),

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(1 + s ^ 2) * √(x ^ 2) = √(1 + s ^ 2) * x
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(1 + s ^ 2) * x = 2 * √(1 + s ^ 2) * (x / 2)

Tactic:
ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u

Tactic:
rw [smul_comm, smul_comm b, smul_comm a b u]

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

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε / 3 = ε - (ε / 3 + ε / 3)

Tactic:
ring

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case refine_2
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2, ‖f x‖ₑ ∂volume.restrict (uIoc a b)).toReal

Tactic:
have : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
      E ∈ disjWithin a b :=
    eventually_inf_principal.mpr (by simp)

Goal state after:
case refine_2
f : ℝ → ℝ
a b c : ℝ
h : IntervalIntegrable f volume a b
hc : c ∈ uIcc a b
s : ℕ × (ℕ → ℝ × ℝ) → Set ℝ := fun E ↦ ⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2
this✝¹ :
  Tendsto (fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this✝ :
  Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : ℝ) in s i, ‖f x‖ₑ ∂volume.restrict (uIoc a b))
    (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)
this : ∀ᶠ (E : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b), E ∈ disjWithin a b
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ x ∈ Finset.range t.1, dist (∫ (v : ℝ) in c..(t.2 x).1, f v) (∫ (v : ℝ) in c..(t.2 x).2, f v) ≤
      (∫⁻ (x : ℝ) in ⋃ i ∈ Finset.range t.1, uIoc (t.2 i).1 (t.2 i).2, ‖f x‖ₑ ∂volume.restrict (uIoc a b)).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)

Tactic:
ring

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

Goal state before:
pp: case h
θ : ℂ
k : ℤ
hk : θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2
⊢ (2 * ↑k + 1) * ↑π / 2 + ↑π / 2 = (↑k + 1) * ↑π

Tactic:
ring

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

Goal state before:
pp: case h
k : ℤ
⊢ ↑k * ↑π - ↑π / 2 = (2 * (↑k - 1) + 1) * ↑π / 2

Tactic:
ring

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

Goal state before:
pp: case refine_1
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π + (2 * x - ↑π) + ↑π = 2 * (2 * ↑k * ↑π + x)

Tactic:
ring

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

Goal state before:
pp: case refine_2
x y : ℂ
k : ℤ
⊢ 2 ^ 2 * ↑k * ↑π - (2 * x - ↑π) + ↑π = 2 * (↑π * (2 * ↑k + 1) - x)

Tactic:
ring

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

Goal state before:
pp: case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖

Tactic:
← dist_ne_zero

Goal state after:
case inr
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : dist w z ≠ 0
⊢ ‖f w‖ = ‖f z‖
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
h_anti : AntitoneOn (deriv f) (interior D)
⊢ MonotoneOn (deriv (-f)) (interior D)

Tactic:
by
    simpa only [← deriv.neg] using h_anti.neg

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

Goal state before:
pp: x y : ℂ
x_ne : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
minus_y_ne : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
l : ℤ
⊢ -((2 * ↑l + 1) * ↑π / 2) = (2 * (-↑l - 1) + 1) * ↑π / 2

Tactic:
ring

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

Goal state before:
pp: case h
x : ℂ
x_eq : ∃ k, x = (2 * ↑k + 1) * ↑π / 2
l : ℤ
⊢ -((2 * ↑l + 1) * ↑π / 2) = (2 * (-↑l - 1) + 1) * ↑π / 2

Tactic:
ring

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

Goal state before:
pp: case e'_3.e'_6
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
this : tan (x + -y) = (tan x + -tan y) / (1 - tan x * -tan y)
⊢ 1 + tan x * tan y = 1 - tan x * -tan y

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x w, deriv f a < (f w - f x) / (w - x)

Tactic:
apply StrictMonoOn.exists_deriv_lt_slope_aux _ hxw _ _

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ContinuousOn f (Icc x w)

x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ StrictMonoOn (deriv f) (Ioo x w)

x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∀ w_1 ∈ Ioo x w, deriv f w_1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - (tan (x / 2) * cos (x / 2)) ^ 2 = (1 - tan (x / 2) ^ 2) * cos (x / 2) ^ 2

Tactic:
ring

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

Goal state before:
pp: case neg
x : ℂ
h : ¬cos (x / 2) = 0
⊢ 2 * (tan (x / 2) * cos (x / 2)) * cos (x / 2) = 2 * tan (x / 2) * cos (x / 2) ^ 2

Tactic:
ring

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

Goal state before:
pp: z w : ℂ
⊢ cexp (z * I) ^ 2 + 1 - cexp (z * I) * 2 * w = cexp (z * I) * (cexp (z * I) - 2 * w) + 1

Tactic:
ring

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

Goal state before:
pp: x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1

Tactic:
ring

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

Goal state before:
pp: case e'_9
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2

Tactic:
ring

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

Goal state before:
pp: x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1

Tactic:
rwa [hx]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x

Tactic:
rw [← inv_div]

Goal state after:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x

Tactic:
rw [← inv_div]

Goal state after:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False

Tactic:
· rw [lt_iff_not_ge] at hx_gt
    refine hx_gt ?_
    rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, neg_mul_eq_neg_mul,
      mul_le_mul_iff_left₀ (half_pos pi_pos)]
    have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
    rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]
    · norm_num
      assumption_mod_cast
    · exact zero_lt_two

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @le_sin_mul ((π / 2)⁻¹ * x)
    (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
    (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])

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

Goal state before:
pp: ⊢ arctan √3 = π / 3

Tactic:
rw [← tan_pi_div_three, arctan_tan]

Goal state after:
case hx₁
⊢ -(π / 2) < π / 3

case hx₂
⊢ π / 3 < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
t : ℝ
⊢ cos t - (1 - 3 * t ^ 2 / 6) = cos t - 1 + t ^ 2 / 2

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : π / 2 - arctan x + (π / 2 - arctan y) = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
⊢ π / 2 - arctan x + (π / 2 - arctan y) = π - (arctan x + arctan y)

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ (-x + -y) / (1 - -x * -y) = -((x + y) / (1 - x * y))

Tactic:
ring

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

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

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

Goal state before:
pp: case e_a
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

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

Goal state before:
pp: case e_a
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

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

Goal state before:
pp: ⊢ 4 * arctan 5⁻¹ = 2 * (2 * ?m.35)

Tactic:
ring

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

Goal state before:
pp: x : ℝ
⊢ 2 * (|x| / 2) = |x|

Tactic:
ring

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

Goal state before:
pp: case inl.inl
a : ℂ
ha : a ≠ 0
⊢ angle (a * 0) (a * 0) = angle 0 0

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

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

Goal state before:
pp: case inl.inr
a : ℂ
ha : a ≠ 0
y : ℂ
hy : y ≠ 0
⊢ angle (a * 0) (a * y) = angle 0 y

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

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

Goal state before:
pp: case inr.inl
a : ℂ
ha : a ≠ 0
x : ℂ
hx : x ≠ 0
⊢ angle (a * x) (a * 0) = angle x 0

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

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

Goal state before:
pp: case inr.inr
a : ℂ
ha : a ≠ 0
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle (a * x) (a * y) = angle x y

Tactic:
simp [angle_eq_abs_arg, mul_div_mul_left, *]

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π) ^ 2 * θ ^ 2 = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2))

Tactic:
ring

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 2 * (1 - (1 - θ ^ 2 / 2)) = θ ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_4
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ -π + 2 * π = π

Tactic:
ring

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ ‖f z / (2 * ↑M - f z)‖ ≤ 1 / R * ‖z‖

Tactic:
by
  rw [← dist_zero_right, ← dist_zero_right]
  nth_rw 1 [← zero_div (2 * M - f 0), ← hf₂]
  apply dist_le_div_mul_dist_of_mapsTo_ball (R₂ := 1) ?_ (fun x hx ↦ ?_) hz
  · apply hf.div (hf.const_sub _) fun x hx h ↦ ?_
    have := sub_eq_zero.mp h ▸ hf₁ hx
    aesop
  · simpa [hf₂] using
      div_le_one_of_le₀ (norm_le_norm_two_mul_sub hM (hf₁ hx)) (by positivity)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x‖ ^ 2 - 2 * -(‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
ring

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' < slope f x y

Tactic:
by
  obtain ⟨u, hxu, huy⟩ := exists_between hxy
  have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
  have := hfc.secant_strict_mono hx hu hy hxu.ne' hxy.ne' huy
  simp only [← slope_def_field] at this
  exact (hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 + 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ‖x‖ ^ 2 - 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2

Tactic:
ring

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))

Tactic:
ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 = -(‖x‖ * ‖y‖)

Tactic:
ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 = ‖x‖ * ‖y‖

Tactic:
ring

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ 2 * (M + ‖f 0‖) * ‖z‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)

Tactic:
ring

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)

Tactic:
field_simp; ring

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ ↑n, ⋯⟩

pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩

Tactic:
· convert! isCoveringMap_npow n _ <;> aesop

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
⊢ (divisor (f₁ + f₂) U)⁻ z ≤ ((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻) z

Tactic:
simp only [Function.locallyFinsuppWithin.negPart_apply, Function.locallyFinsuppWithin.max_apply]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
⊢ ((divisor (f₁ + f₂) U) z)⁻ ≤ max ((divisor f₁ U) z)⁻ ((divisor f₂ U) z)⁻
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
⊢ ∃ n g_1, AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ g • f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_1

Tactic:
use n, g • g_f, h₁g.smul h₁g_f

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
⊢ (g • g_f) x ≠ 0 ∧ g • f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g • g_f
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g) y
⊢ (g y)⁻¹ * ((y - x) ^ n)⁻¹ = ((y - x) ^ n)⁻¹ * (g y)⁻¹

Tactic:
ring

Goal state after: