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

Goal state before:
pp: case ac
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) < ε / 2

pp: case bd
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) < ε / 2

Tactic:
· calc
      μ (U \ s) ≤ μ (U \ K) := by gcongr
      _ < ε / 2 := by
        apply measure_sdiff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
        exact ne_top_of_le_ne_top hμs (by gcongr)

Goal state after:
case bd
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) < ε / 2
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
⊢ (μ.withDensity f) s = 0

Tactic:
let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)

Goal state after:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ (μ.withDensity f) s = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ∞
this : Fact (μ A < ∞)
V : Set α
V_open : IsOpen[inst✝²] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsClosed[inst✝²] K ∧ r < (μ.restrict A) K

Tactic:
have : InnerRegularWRT (μ.restrict A) IsClosed (fun s ↦ MeasurableSet s) :=
    InnerRegularWRT.restrict_of_measure_ne_top innerRegular_measurable h'A

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ∞
this✝ : Fact (μ A < ∞)
V : Set α
V_open : IsOpen[inst✝²] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
this : (μ.restrict A).InnerRegularWRT IsClosed[inst✝²] fun s ↦ MeasurableSet s
⊢ ∃ K ⊆ V, IsClosed[inst✝²] K ∧ r < (μ.restrict A) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬μ univ = 0

Tactic:
isOpen_univ.measure_eq_iSup_isCompact,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬⨆ K, ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), μ K = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ Measurable fun b ↦ μ.withDensity (f b)

Tactic:
Measure.measurable_measure

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
quadratic_eq_zero_iff_discrim_eq_sq ha,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ discrim a b c = (2 * a * x + b) ^ 2 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
rw [inv_eq_one_div]

Goal state after:
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (1 / 2))
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp
x : ℝ
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
rcases le_or_gt 0 x with hle | hlt

Goal state after:
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ √x = y

Tactic:
rw [h, sqrt_mul_self hy]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y

Tactic:
constructor
  · simpa only [abs_le] using abs_le_sqrt
  · rw [← abs_le, ← sq_abs]
    exact (le_sqrt (abs_nonneg x) h).mp

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

Goal state before:
pp: x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(x ^ 2 + y ^ 2)

Tactic:
by
  rw [← normSq_add_mul_I]; rfl

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
⊢ (fun x ↦ ‖x‖) (↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j) < ε

Tactic:
obtain ⟨H₁, H₂⟩ := H _ ij

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
H₁ : |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2
H₂ : |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
⊢ (fun x ↦ ‖x‖) (↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j) < ε
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).re = (↑p.1 + ↑p.2 * I).re

Tactic:
simp [Complex.equivRealProd, ofReal]

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

Goal state before:
pp: case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).im = (↑p.1 + ↑p.2 * I).im

Tactic:
simp [Complex.equivRealProd, ofReal]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞}, Measurable f → SFinite (μ.withDensity f)
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
h : μ.withDensity g = μ.withDensity f
⊢ SFinite (μ.withDensity f)

Tactic:
exact h ▸ this hgm

Goal state after:
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 φ
x : α
⊢ (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν

Tactic:
rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁴ : RCLike K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = ↑r • x

Tactic:
RCLike.ofReal_alg,

Goal state after:
K : Type u_1
E : Type u_2
inst✝⁴ : RCLike K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = (r • 1) • x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(r * re z) - ↑(r * im z) * I = r • (↑(re z) - ↑(im z) * I)

Tactic:
ofReal_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑r * ↑(re z) - ↑(r * im z) * I = r • (↑(re z) - ↑(im z) * I)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑r * ↑(re z) - ↑(r * im z) * I = r • (↑(re z) - ↑(im z) * I)

Tactic:
ofReal_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑r * ↑(re z) - ↑r * ↑(im z) * I = r • (↑(re z) - ↑(im z) * I)
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
RCLike.le_iff_re_im

Goal state after:
x y : ℂ
h : RCLike.re x ≤ RCLike.re y ∧ RCLike.im x = RCLike.im y
⊢ x.re ≤ y.re
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
x : ↥(selfAdjoint A)
⊢ ↑(ℑ (I • ↑x)) = ↑x

Tactic:
simp only [imaginaryPart_I_smul, x.property.coe_realPart]

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:
RCLike.le_iff_re_im

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
h : re x ≤ re y ∧ im x = im y
⊢ re x ≤ re y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y

Tactic:
RCLike.le_iff_re_im

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
p : K × K
| p.1 ≤ p.2

Tactic:
RCLike.le_iff_re_im

Goal state after:
K : Type u_1
inst✝ : RCLike K
p : K × K
| re p.1 ≤ re p.2 ∧ im p.1 = im p.2
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e.toIsometryEquiv = univ

Tactic:
exact IsometryEquiv.range_eq_univ _

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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ n ≤ k + max n i

Tactic:
by omega

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c
hb' : b ≠ a
⊢ ‖f b‖ ≤ max c ‖f a‖

Tactic:
exact (hb hb').trans (le_max_left ..)

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

Goal state before:

Tactic:
‖∑ i ∈ s, A i x‖ ≤ ∑ i ∈ s, ‖A i x‖ := norm_sum_le ..
    _ ≤ ∑ i ∈ s, C i * ‖B i x‖ := Finset.sum_le_sum (fun j hj ↦ hx j hj)
    _ ≤ ∑ i ∈ s, sSup (C '' s) * ‖B i x‖ := by
        refine Finset.sum_le_sum ?_
        intro j hj; gcongr
        rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]; use j
    _ = sSup (C '' s) * ∑ i ∈ s, ‖B i x‖ := (Finset.mul_sum ..).symm
    _ = sSup (C '' s) * ‖∑ i ∈ s, ‖B i x‖‖ := by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ (x : α), 1 ≤ g x / f x → g x = 0 → f x = 0

Tactic:
intro x h h0

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h✝ : Tendsto (fun x ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
h0 : g x = 0
⊢ f x = 0
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
rw [← lim_const (abv := norm) (∑ m ∈ range n, _), exp, sub_eq_add_neg,
    ← lim_neg, lim_add, ← lim_norm]

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

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

Tactic:
have s1 := sin_add ((x + y) / 2) ((x - y) / 2)
  have s2 := sin_sub ((x + y) / 2) ((x - y) / 2)
  rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1
  rw [div_sub_div_same, ← sub_add, add_sub_cancel_left, add_self_div_two] at s2
  rw [s1, s2]
  ring

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

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

Tactic:
by
  simp [← ENNReal.toReal_eq_one_iff]

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

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

Tactic:
by
  simp [← ENNReal.toReal_eq_one_iff]

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

Goal state before:
pp: case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x

Tactic:
simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx']
    using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

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

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ ‖cexp x - cexp y‖ < ε

Tactic:
have : cexp x - cexp y = cexp y * (cexp (x - y) - 1) := by
    rw [mul_sub_one, ← exp_add]
    ring_nf

Goal state after:
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖cexp x - cexp y‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
x : ℝ
⊢ x ^ n * (rexp x)⁻¹ = x ^ n * rexp (-x)

Tactic:
exp_neg

Goal state after:
n : ℕ
x : ℝ
⊢ x ^ n * (rexp x)⁻¹ = x ^ n * (rexp x)⁻¹
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ

Tactic:
by
  simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]

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

Goal state before:
pp: n : ℕ
⊢ √(2 + sqrtTwoAddSeries 0 n) < √(2 ^ 2)

Tactic:
sqrt_lt_sqrt_iff,

Goal state after:
n : ℕ
⊢ 2 + sqrtTwoAddSeries 0 n < 2 ^ 2

n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto
  simp

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

Goal state before:
pp: ⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Tactic:
convert! continuous_sin.continuousWithinAt.tendsto using 2
  simp

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

Goal state before:
pp: ⊢ Function.Periodic cosh (2 * ↑π * I)

Tactic:
by
  convert! cosh_antiperiodic.periodic_two_mul using 1
  ring

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
U : Set Y
inst✝ : CompactSpace X
hU : IsOpen[inst✝¹] U
⊢ IsOpen {f | MapsTo (⇑f) univ U}

Tactic:
exact isOpen_setOfPred_mapsTo isCompact_univ hU

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y

Tactic:
by
  refine ⟨?_, (.map · hf.continuous)⟩
  rintro ⟨γ, hγ⟩
  choose γ' hγ'F hγ' using hγ
  have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
  have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
  have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
  exact (h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s

Tactic:
rw [← Homeomorph.image_symm]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s
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:
← range_subset_iff

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
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
⊢ ConnectedSpace X

Tactic:
by
  rw [connectedSpace_iff_connectedComponent]
  rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩
  use x
  rw [← univ_subset_iff]
  exact (by simpa using hx : pathComponent x = univ) ▸ pathComponent_subset_component x

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: 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₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : t₀ ≤ t₁
⊢ γ.extend ↑0 = γ.extend t₀

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

pp: 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₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₀

pp: 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₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

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

pp: 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₀ ≤ ↑0
h✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· simp [γ.extend_of_le_zero h₁]

Goal state after:
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₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend ↑0 = γ.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₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
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₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : ¬t₀ ≤ 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₀ ≤ ↑0
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₀ ≤ ↑0
h✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
Module: Mathlib.Topology.Path

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

Tactic:
by
  have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop
  exact γ.truncate_continuous_family.comp key

Goal state after: