mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
· refine lintegral_congr (fun x ↦ ?_)
    rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]
    simp

Goal state after:
case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) = (z + (starRingEnd K) z) / 2

Tactic:
rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: x : ℂ
⊢ x ∈ ℝ[I]

Tactic:
← x.re_add_im,

Goal state after:
x : ℂ
⊢ ↑x.re + ↑x.im * I ∈ ℝ[I]
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
← RCLike.ofReal_eq_complex_ofReal

Goal state after:
x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x y : ℂ
h : x ≤ y
⊢ x.re ≤ y.re

Tactic:
rw [RCLike.le_iff_re_im] at h
  exact h.1

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsHomeomorph ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
rw [isHomeomorph_iff_isEmbedding_surjective]
    refine ⟨?_, Equiv.surjective _⟩
    rw [PartialEquiv.toEquiv_eq_codRestrict_restrict]
    apply IsEmbedding.codRestrict
    simpa! [domRestrict_eq] using h.comp subtypeVal

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

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w → (re z ≤ re w ∧ im z = im w) ∧ z ≠ w

Tactic:
· rintro ⟨⟨hr, hrn⟩, hi⟩
    exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
rw [e.eventually_nhdsWithin _ hx]
  refine eventually_congr <|
    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
  rw [hy]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
h : x ≤ y
⊢ re x ≤ re y

Tactic:
rw [RCLike.le_iff_re_im] at h
  exact h.1

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
c : ℝ
f'' : α → E''
g'' : α → F''
l : Filter α
h : IsBigOWith c l f'' g''
x : α
hx : ‖f'' x‖ ≤ c * ‖g'' x‖
hg : g'' x = 0
⊢ ‖f'' x‖ ≤ 0

Tactic:
by simpa [hg] using hx

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖1‖ ≤ ‖f x‖) ↔ ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, ‖f x‖ ∈ Ici ↑n

Tactic:
simp only [norm_one, mul_one, true_imp_iff, mem_Ici]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
C : ι → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ c, IsBigOWith c l (∑ i ∈ s, A i) g

Tactic:
exact ⟨_, IsBigOWith.sum hC⟩

Goal state after:
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
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / (4 * Q) * (2 * Q) = ε

Tactic:
two_mul_two,

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
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / (2 * 2 * Q) * (2 * Q) = ε
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sin (x + y) * I = (sin x * cos y + cos x * sin y) * I

Tactic:
← sinh_mul_I,

Goal state after:
x y : ℂ
⊢ sinh ((x + y) * I) = (sin x * cos y + cos x * sin y) * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sinh (x * I + y * I) = sin x * I * cos y + cos x * sin y * I

Tactic:
← sinh_mul_I,

Goal state after:
x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sin y * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * (sin y * I)

Tactic:
← sinh_mul_I,

Goal state after:
x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sinh (y * I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
by
  calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
  · congr <;> field
  · rw [cos_add, cos_sub]
  ring

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

Goal state before:
pp: x : ℂ
⊢ sin ((starRingEnd ℂ) x) * I = (starRingEnd ℂ) (sin x) * I

Tactic:
← sinh_mul_I,

Goal state after:
x : ℂ
⊢ sinh ((starRingEnd ℂ) x * I) = (starRingEnd ℂ) (sin x) * I
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
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:
· rw [← mul_sum]
    gcongr
    simp_rw [← div_pow]
    rw [geom_sum_eq, div_le_iff_of_neg]
    · trans (-1 : ℝ)
      · linarith
      · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
        positivity
    · linarith
    · linarith

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range j with n ≤ i, ‖x ^ i / ↑i.factorial‖ = ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / ↑k.factorial

Tactic:
congr with i

Goal state after:
case e_f
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
⊢ ‖x ^ i / ↑i.factorial‖ = ‖x‖ ^ i / ↑i.factorial
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =o[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =o[l] g'

Tactic:
by
  simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]
  exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn <;> simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
h : ∀ (x_1 : ℝ), x_1 - ‖x‖ < δ ∧ ‖x‖ - x_1 < δ → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε

Tactic:
obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this✝ : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
⊢ y ∈ u

Tactic:
apply hε

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this✝ : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
⊢ y ∈ closedBall x ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (π - 2 * θ) = sin (2 * θ + θ)

Tactic:
by congr; linarith

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ 0 < sin y * cos x - cos y * sin x

Tactic:
← sin_sub

Goal state after:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ 0 < sin (y - x)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

Tactic:
cthickening_zero,

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = thickening (ε + 0) s
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.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]

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'

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y
Module: Mathlib.Topology.Connected.PathConnected

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

Tactic:
intro h'

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ

Tactic:
rw [← range_subset_iff] at hγ₁

Goal state after:
case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : range ⇑γ₁ ⊆ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ 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
this : IsPathConnected univ
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p (last n))
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc 0 1 ⊆ IccExtend ⋯ f '' Icc 0 1
w : ℝ
hw₁ : w ∈ Icc 0 1
hw₂ : f ⟨w, hw₁⟩ = t
⊢ ∃ a, f a = t

Tactic:
exact ⟨_, hw₂⟩

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

Goal state before:
pp: case inl.left
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ f (2 * n)

pp: case inl.right
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)

Tactic:
· rwa [sub_le_iff_le_add, add_comm]

Goal state after:
case inl.right
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = arcsin x

Tactic:
rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]

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

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

Tactic:
rw [not_le] at hx₂

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ 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₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₂

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hg
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖g x‖) l (𝓝 0)

Tactic:
rw [← tendsto_zero_iff_norm_tendsto_zero]

Goal state after:
case hg
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto g l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬z.arg = -(π / 2) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
arg_eq_neg_pi_div_two_iff

Goal state after:
z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (-θ).toReal = -θ.toReal ↔ θ ≠ ↑π

Tactic:
nth_rw 1 [← coe_toReal θ, ← coe_neg, toReal_coe_eq_self_iff]

Goal state after:
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases hx.eq_or_lt with (rfl | pos)
  · rw [zero_rpow h, zero_eq_mul]
    have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
    exact this.imp zero_rpow zero_rpow
  · exact rpow_add pos _ _

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

Goal state before:
pp: case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y

Tactic:
intro a ha

Goal state after:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl.inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inr.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inr.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
all_goals grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Goal state after: