mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

Tactic:
hasFiniteIntegral_iff_ofReal

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 0 ≤ᵐ[μ] bound
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ √(normSq z) = √(z.re ^ 2 + z.im ^ 2)

Tactic:
normSq_apply,

Goal state after:
z : ℂ
⊢ √(z.re * z.re + z.im * z.im) = √(z.re ^ 2 + z.im ^ 2)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.im ^ 2 ≤ normSq z

Tactic:
normSq_apply,

Goal state after:
z : ℂ
⊢ z.im ^ 2 ≤ z.re * z.re + z.im * z.im
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.re| ^ 2 < normSq z ↔ z.im ≠ 0

Tactic:
normSq_apply,

Goal state after:
z : ℂ
⊢ |z.re| ^ 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.im| < ‖z‖ ↔ z.re ≠ 0

Tactic:
simpa using @abs_re_lt_norm (z * I)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f)

Tactic:
simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]

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 : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
fun_prop

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 ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
fun_prop

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

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
⊢ AEMeasurable (fun y ↦ f y * g (y⁻¹ * a)) μ

Tactic:
fun_prop

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

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (a, a⁻¹ * x)) (μ.prod μ)

Tactic:
fun_prop

Goal state after:
case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (a, a⁻¹ * x)) (μ.prod μ)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)

Tactic:
fun_prop

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

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

Tactic:
fun_prop

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

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

Tactic:
fun_prop

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

Goal state before:
pp: case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

Tactic:
fun_prop

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

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1 * g z.2) (μ.prod μ)

Tactic:
fun_prop

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

Goal state before:
pp: case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ ↑(star (x * y)) = ↑(star y * star x)

Tactic:
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst✝⁷ : UniformSpace E₁
inst✝⁶ : UniformSpace E₂
inst✝⁵ : Ring E₁
inst✝⁴ : IsUniformAddGroup E₁
inst✝³ : Algebra R E₁
inst✝² : Ring E₂
inst✝¹ : IsUniformAddGroup E₂
inst✝ : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑e
h₂ : Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
⊢ Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Instances.RealVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousSMul ℝ F
inst✝² : T2Space F
G : Type u_3
inst✝¹ : FunLike G E F
inst✝ : AddMonoidHomClass G E F
f : G
hf : Continuous ⇑f
c : ℝ
x : E
⊢ Continuous fun c ↦ f (c • x)

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ MulOpposite.op r • x = r • x

Tactic:
by ext <;> simp [smul_re, smul_im, op_smul_eq_smul]

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
x : A
hx : IsSelfAdjoint x
⊢ ℑ x = 0

Tactic:
by
  rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
hr : 0 < r
a b : K
hab : a < b
⊢ r • a < r • b

Tactic:
simpa [RCLike.lt_iff_re_im (K := K), smul_re, smul_im, hr, hr.ne'] using hab

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.1

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.2

Tactic:
fun_prop

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.1

Tactic:
fun_prop

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

Goal state before:
pp: case refine_4
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.2

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ Function.Involutive star

Tactic:
exact h.star_involutive

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₁ : (n.succ : α) ≠ 1 :=
        @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: ⊢ cos 0 = 1

Tactic:
by simp [cos]

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

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

Tactic:
add_right_comm,

Goal state after:
x y : ℂ
s1 : sin ((x + x + y - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
s1 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
have s2 := cos_sub ((x + y) / 2) ((x - y) / 2)

Goal state after:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
s1 : cos ((x + y + x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
add_right_comm,

Goal state after:
x y : ℂ
s1 : cos ((x + x + y - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos (-x) = cos x

Tactic:
by simp [cos]

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

Goal state before:
pp: z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]

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

Goal state before:
pp: n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)
⊢ |1 + x / ↑m * 0 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)

Tactic:
by simpa using e

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

Goal state before:
pp: a : ℝ
⊢ Continuous cexp

Tactic:
fun_prop

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
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ IsCauSeq abv fun m ↦ ∑ n ∈ range m, f n

Tactic:
have har1 : |r| < 1 := by rwa [abs_of_nonneg hr0]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
⊢ IsCauSeq abv fun m ↦ ∑ n ∈ range m, f n
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Continuous fun x ↦ (Complex.exp ↑x).re

Tactic:
fun_prop

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

Goal state before:
pp: s : Set ℝ
⊢ ContinuousOn rexp s

Tactic:
fun_prop

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

Goal state before:
pp: case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ (fun x ↦ x ^ n / (b * rexp x + c)) = fun x ↦ -(x ^ n / (-b * rexp x + -c))

Tactic:
ext x
      field_simp
      rw [← neg_add (b * exp x) c, div_neg, neg_neg]

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

Goal state before:
pp: ⊢ Continuous fun z ↦ (cexp (-z * I) - cexp (z * I)) * I / 2

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun z ↦ (cexp (z * I) + cexp (-z * I)) / 2

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun z ↦ (cexp z - cexp (-z)) / 2

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun z ↦ (cexp z + cexp (-z)) / 2

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x ↦ 1) =O[l] fun x ↦ rexp (f x)) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) l f

Tactic:
by
  simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s ∈ S, ‖m * s‖ < ‖(mk' S) m‖ + ε

Tactic:
obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε
  exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩

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

Goal state before:
pp: n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0

Tactic:
neg_lt,

Goal state after:
n : ℤ
hx₁ : -(↑n * (2 * π)) < 2 * π
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
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:
singleton_mul_closedBall

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

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
| inr h =>

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ ↑‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal

Tactic:
coe_nnnorm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ ‖c‖ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: 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
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ↑‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal

Tactic:
coe_nnnorm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 6) = 1 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_three]

Goal state after:
⊢ cos (π / 2 - π / 6) = cos (π / 3)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ (ε + δ) / (ε + δ) = 1

Tactic:
div_self hεδ.ne'

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Tactic:
by
  refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩
  rw [add_comm] at hxy
  obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy
  rw [dist_comm] at hxz
  exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1

Tactic:
exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ r • closedBall 0 1 = closedBall 0 r

Tactic:
rw [smul_unitClosedBall, Real.norm_of_nonneg hr]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Continuous[_, instTopologicalSpaceSubtype] fun t ↦ ⟨h.somePath t, ⋯⟩

Tactic:
fun_prop

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 z : X
ι : Type u_3
F : Set X
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ Continuous[_, inst✝¹] fun x ↦ g * γ x * g⁻¹

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Path

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
γ : Path x y
⊢ Continuous[_, inst✝¹] ⇑γ.toContinuousMap

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
⊢ Continuous[_, inst✝¹] (⇑γ ∘ σ)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Path

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
γ✝ γ : Path x y
⊢ ContinuousOn ⇑γ.extend I

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst✝¹] fun t ↦ γ.extend (2 * t)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
γ' : Path y z
⊢ Continuous[_, inst✝¹] fun t ↦ γ'.extend (2 * t - 1)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace T
K : Set X
U : Set Y
f : C(X × Y, Z)
a : X
⊢ Continuous[inst✝², instTopologicalSpaceProd] (Prod.mk a)

Tactic:
fun_prop

Goal state after: