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

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ h * g) ⁻¹' A) = μ A) ↔ μ.IsMulRightInvariant

Tactic:
by
  trans ∀ g, map (· * g) μ = μ
  · simp_rw [Measure.ext_iff]
    refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_
    rw [map_apply (measurable_mul_const g) hA]
  exact ⟨fun h => ⟨h⟩, fun h => h.1⟩

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]

Tactic:
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
x : G
⊢ μ ((fun y ↦ y * x) ⁻¹' s) = μ ((fun x_1 ↦ (x_1, x)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)

Tactic:
congr 1 with y : 1

Goal state after:
case e_6
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul₂ G
μ : Measure G
inst✝ : SFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
x y : G
⊢ y ∈ (fun y ↦ y * x) ⁻¹' s ↔ y ∈ (fun x_1 ↦ (x_1, x)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: case e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ μ = map (⇑(MeasurableEquiv.mulLeft g)) μ

Tactic:
simp [map_mul_left_eq_self μ g]

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

Goal state before:
pp: case zero
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ IsClosed[inst✝⁷] (L 0)

Tactic:
exact Kclosed

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm

Tactic:
lintegral_trim _ hf,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
⊢ ∀ ⦃K : Set H⦄, IsCompact K → (map (⇑f) μ) K < ∞

Tactic:
intro K

Goal state after:
G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
⊢ IsCompact K → (map (⇑f) μ) K < ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : 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
⊢ ∃ U, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Tactic:
by
  have : ε / 2 ≠ 0 := (ENNReal.half_pos hε).ne'
  rcases hs.exists_isCompact_isClosed_sdiff_lt hμs this with ⟨K, hKs, hKco, hKcl, hμK⟩
  rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩
  refine ⟨U, hUo, hμU.trans_le le_top, ?_⟩
  rw [← ENNReal.add_halves ε, measure_symmDiff_eq hUo.nullMeasurableSet hs.nullMeasurableSet]
  gcongr
  · 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)
  · exact lt_of_le_of_lt (by gcongr) hμK

Goal state after:
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 ≠ ∞
⊢ (μ.restrict A).WeaklyRegular

Tactic:
have : Fact (μ A < ∞) := ⟨h'A.lt_top⟩

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ∞
this : Fact (μ A < ∞)
⊢ (μ.restrict A).WeaklyRegular
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
have hg : Measurable g :=
    (hf.comp measurable_inv).div ((measurable_measure_mul_right ν' sm).comp measurable_inv)

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ✝ : Measure α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SigmaCompactSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
⊢ μ.Regular

Tactic:
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ✝ : Measure α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SigmaCompactSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.Regular
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ∞

Tactic:
by
  simp only [hasFiniteIntegral_iff_norm, edist_dist, dist_zero_right]

Goal state after:
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
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0

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
h : ∃! x, discrim a b c = (2 * a * x + b) ^ 2
⊢ discrim a b c = 0
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖₊ = ‖r‖₊

Tactic:
by ext; exact norm_real _

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
restrict_withDensity' s,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
⊢ μ ≪ μ.withDensity f

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : (μ.withDensity f) s = 0
⊢ μ s = 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: x y : ℝ
hxy : x ≤ y
⊢ ↑x ≤ ↑y

Tactic:
simp only [real_le_real, hxy]

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

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

Tactic:
withDensity_sum

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ], IsFiniteMeasure μ → SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite (sum fun n ↦ (sfiniteSeq μ n).withDensity f)
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * (star U * U) * B = 1

Tactic:
by rw [hA₁, mul_one, hB₁]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b

Tactic:
by
  rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]

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

Goal state before:
pp: ⊢ (LinearMap.toMatrix basisOneI basisOneI) ↑↑conjAe = !![1, 0; 0, -1]

Tactic:
by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ re x = y ↔ x = ↑y

Tactic:
simp [RCLike.ext_iff (K := K), hx, im_eq_zero_iff_isSelfAdjoint]

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
hr : -↑r ∈ s
⊢ -↑r ≤ 0

Tactic:
simpa using hs hr

Goal state after:
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
B : Type u_2
F : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module ℂ B
inst✝⁴ : StarAddMonoid B
inst✝³ : StarModule ℂ B
inst✝² : FunLike F A B
inst✝¹ : StarHomClass F A B
inst✝ : LinearMapClass F ℂ A B
f : F
x : A
⊢ f ↑(ℑ x) = ↑(ℑ (f x))

Tactic:
by
  simp [imaginaryPart_apply_coe, ← Complex.coe_smul, map_star]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0

Tactic:
simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ ↑e y ∈ e.target ∧ ↑e.symm (↑e y) ∈ s ∧ ↑e.symm (↑e y) ∈ f ⁻¹' t

Tactic:
e.mapsTo hy,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ True ∧ ↑e.symm (↑e y) ∈ s ∧ ↑e.symm (↑e y) ∈ f ⁻¹' t
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ Tendsto f (𝓝[s] ↑e (↑e.symm x)) (𝓝 (f (↑e (↑e.symm x))))

Tactic:
e.right_inv h

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
rw [ofReal_mul_pos_iff] at h

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp only [IsBigO_def, IsBigOWith_def]

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
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
isBigO_iff,

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ (∃ c, ∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
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
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
isBigO_iff,

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ (∃ c, ∀ᶠ (x : α) in ⊤, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ (cexp ↑x).im = 0

Tactic:
← ofReal_exp_ofReal_re,

Goal state after:
x : ℝ
⊢ (↑(cexp ↑x).re).im = 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x

Tactic:
have := @isLittleO_norm_pow_norm_pow E' _ _ _ h

Goal state after:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ ‖x‖ ^ 1
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cexp x = cexp (↑x.re + ↑x.im * I)

Tactic:
re_add_im

Goal state after:
x : ℂ
⊢ cexp x = cexp x
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
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x ↦ f x i) g'

Tactic:
exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → E
g : α → F
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
isBigO_iff,

Goal state after:
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → E
g : α → F
⊢ (∃ c, ∀ᶠ (x : α) in atTop, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g 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
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
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
this :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) +
      (∑ i ∈ range K, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) -
        ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) <
    ε / (2 * P) * P + ε / (4 * Q) * (2 * Q)
⊢ ∑ i ∈ range K, abv (f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k)) < ε

Tactic:
rw [hε] at this
    simpa [abv_mul abv] using this

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 0 < sin x

Tactic:
calc 0 < x - x ^ 3 / 6 - |x| ^ 5 / 100 := by grind [pow_le_of_le_one]
    _ ≤ sin x :=
      sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound (by rwa [abs_of_nonneg (le_of_lt hx0)]))).2

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp 0 * (cexp (-(↑x / 2) * I) - cexp (↑x / 2 * I)) * I‖

Tactic:
rw [← neg_add_cancel (x / 2 * I), exp_add, mul_assoc _ _ (_ - _), mul_sub, ← exp_add, ← exp_add,
    ← add_mul, ← add_mul]

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp ((↑x / 2 + -(↑x / 2)) * I) - cexp ((↑x / 2 + ↑x / 2) * I)) * I‖
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: case refine_1
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

pp: case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Tactic:
· exact fun i ↦ norm_nonneg _

Goal state after:
case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Summable f

Tactic:
refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
    · exact fun i ↦ norm_nonneg _
    · simpa only using! hr

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

Goal state before:
pp: case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
· exact (exp_bound_div_one_sub_of_interval' h1 h2).le

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ rexp x < (2 + x) / (2 - x)

Tactic:
by calc
  _ = exp (x / 2) ^ 2 := by grind [Real.exp_nat_mul (x / 2) 2]
  _ ≤ _ := by
    grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)]
    apply Real.exp_nonneg
  _ < (2 + x) / (2 - x) := by
    rw [lt_div_iff₀ (by linarith), ← sub_pos]
    simp only [Finset.sum_range_succ]
    ring_nf
    positivity

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 = cexp y * (cexp (x - y) - 1)

Tactic:
mul_sub_one,

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)
⊢ cexp x - cexp y = cexp y * cexp (x - y) - cexp y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h0x : 0 < x
hxp : x < π
hx2 : ¬x ≤ 2
⊢ π - x ≤ 2

Tactic:
by linarith [pi_le_four]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ |c| ≤ 1

Tactic:
← Real.norm_eq_abs,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ∀ (n : ℤ), ↑n * π ≠ π / 5

Tactic:
intro n hn

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * π = π / 5
⊢ False
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 ≤ 0
h : dist x z ≤ 0 + δ
⊢ dist x z ≤ δ

Tactic:
rwa [zero_add] at h

Goal state after: