mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : G), s.indicator (fun x ↦ 1) a ∂μ) * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x ↦ 1) x * f y ∂ν ∂μ = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ

Tactic:
exact lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Goal state after:
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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

Tactic:
refine ae_of_forall_measure_lt_top_ae_restrict' ν'.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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 → μ' s_1 < ∞ → ν'.inv s_1 < ∞ → ∀ᵐ (x : G) ∂μ'.restrict s_1, ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
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✝ : SigmaFinite μ
⊢ μ.InnerRegular

Tactic:
refine ⟨(InnerRegularWRT.isCompact_isClosed μ).trans ?_⟩
  refine InnerRegularWRT.of_restrict (fun n ↦ ?_) (iUnion_spanningSets μ).superset
    (monotone_spanningSets μ)
  have : Fact (μ (spanningSets μ n) < ∞) := ⟨measure_spanningSets_lt_top μ n⟩
  exact WeaklyRegular.innerRegular_measurable.trans InnerRegularWRT.of_sigmaFinite

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
X : α → ℝ≥0∞
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
this : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ∞
ω : α
h₁ : a ≤ X ω
h₂ : X ω ≤ b
⊢ ‖X ω‖ₑ ≤ max ‖a‖ₑ ‖b‖ₑ

Tactic:
by simp [h₂]

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

Goal state before:
pp: x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)

Tactic:
exact sqrt_le_left

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

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * (b + c) = a * b + a * c

Tactic:
by intros; ext <;> simp [mul_re, mul_im] <;> ring

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

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), (a + b) * c = a * c + b * c

Tactic:
by intros; ext <;> simp [mul_re, mul_im] <;> ring

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑↑n = 0
⊢ n = 0

Tactic:
ofReal_eq_zero,

Goal state after:
α : Type u_1
n : ℕ
h : ↑n = 0
⊢ n = 0
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ ∅, p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

pp: case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
· simp [h_zero]

Goal state after:
case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0 * ‖x✝‖

Tactic:
zero_mul

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ 0 * ‖x‖ = 0

Tactic:
zero_mul

Goal state after:
V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : dist (r • f x) 0 ≤ dist r 0 * dist (f x) 0
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
dist_zero_right,

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * dist (f x) 0
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
⊢ g (f v) = 0

Tactic:
← comp_apply g f,

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
⊢ (g.comp f) v = 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ x ∈ s

Tactic:
by rw [← hy]; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

Tactic:
rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
⊢ f = g

Tactic:
ext ⟨x, y⟩

Goal state after:
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
x y : ℝ
⊢ f { re := x, im := y } = g { re := x, im := y }
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
⊢ r₁ < ‖↑x‖ ∧ ‖↑x‖ < r₂

Tactic:
by rwa [norm_real, Real.norm_of_nonneg (h₀.trans_lt h.1).le]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : Nonempty ↑s
⊢ (s.partialHomeomorphSubtypeCoe hs).target = s

Tactic:
by
  simp [partialHomeomorphSubtypeCoe]

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
hx : x ∈ e.source
⊢ 𝓝 (↑e.symm (↑e x)) = 𝓝 x

Tactic:
by rw [e.left_inv hx]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : RCLike K
z : K
h : z = ↑‖z‖
⊢ ‖z‖ ≤ re z

Tactic:
· rw [h]
    simp

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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
by subst h''; exact h.re

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

Goal state before:
pp: case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ 0 * ‖f x‖ ≤ ‖g x‖

Tactic:
zero_mul

Goal state after:
case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ 0 ≤ ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x ↦ ‖g' x‖) ↔ f =O[l] g'

Tactic:
simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_right

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
c : ℝ
f : α → E
g : α → F
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_top]

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

Goal state before:
pp: case hbc
α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c c' : ℝ
l : Filter α
inst✝ : NormOneClass S
n : ℕ
f : α → S
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ ‖g x ^ n‖ ≤ ‖g x‖ ^ n

Tactic:
exact norm_pow_le' _ hn.bot_lt

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
constructor
  · rintro h
    rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
    rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩
    exact ⟨φ, ⟨c, hφ⟩, huvφ⟩
  · rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩
    exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

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

Goal state before:
pp: case hdb
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := ⋯
hj : j = n + k
i : ℕ
a✝ : i ∈ range k
⊢ ↑n.factorial * ↑n.succ ^ i ≤ ↑(n + i).factorial

Tactic:
exact mod_cast Nat.factorial_mul_pow_le_factorial

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (↑x).cot = (↑x).cot

Tactic:
← cot_conj,

Goal state after:
x : ℝ
⊢ ((starRingEnd ℂ) ↑x).cot = (↑x).cot
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im

Tactic:
by
  rw [exp_eq_exp_re_mul_sin_add_cos]
  simp [exp_ofReal_re, sin_ofReal_re]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
  simp_rw [← sub_eq_add_neg]
  calc ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
  _ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
by
  have h3 : |x| = x := by simpa
  have h4 : |x| ≤ 1 := by rwa [h3]
  have h' := Real.exp_bound h4 hn
  rw [h3] at h'
  have h'' := (abs_sub_le_iff.1 h').1
  have t := sub_le_iff_le_add'.1 h''
  simpa [mul_div_assoc] using t

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

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

Goal state before:
pp: case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
have hC₁ : C₁ ≤ max C₀ C₁ := by grind
      grw [← hC₁]
      grind

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)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
obtain rfl | hr := hr0.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
⊢ abv (f m) ≤ abv (f n.succ) * 0⁻¹ ^ n.succ * 0 ^ m

case inr
α : 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
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: y : ℝ
⊢ y ≤ rexp (y - 1)

Tactic:
simpa using add_one_le_exp (y - 1)

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

Goal state before:
pp: ⊢ Tendsto rexp (𝓝 0) (𝓝 1)

Tactic:
convert! continuous_exp.tendsto 0
  simp

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
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ m ∈ ↑S ↔ m ∈ S

Tactic:
SetLike.mem_coe

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ m ∈ S ↔ m ∈ S
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ x • sphere y δ = sphere (x • y) δ

Tactic:
smul_sphere

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ |1 - r| * ‖x - y‖ = (1 - r) * dist y x

Tactic:
abs_eq_self.mpr (sub_nonneg.mpr h.2),

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * ‖x - y‖ = (1 - r) * dist y x
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
⊢ y ∈ u

Tactic:
have I : ‖r • z‖ ≤ ε :=
    calc
      ‖r • z‖ = ‖r‖ * ‖z‖ := norm_smul _ _
      _ ≤ ε / R * R := by
        gcongr
        exacts [mem_closedBall_zero_iff.1 hr, mem_closedBall_zero_iff.1 (hR zs)]
      _ = ε := by field

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‖ ≤ ε
⊢ y ∈ u
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ √3 / 2 / cos (π / 3) = √3

Tactic:
cos_pi_div_three

Goal state after:
⊢ √3 / 2 / (1 / 2) = √3
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 (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]

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
⊢ sin x / cos x < sin y / cos y

Tactic:
div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy),

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
by
  set v : ℕ → α := fun n ↦ if n < N then 0 else u n
  have hC : 0 ≤ C :=
    (mul_nonneg_iff_of_pos_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)
  have : ∀ n ≥ N, u n = v n := by
    intro n hn
    simp [v, if_neg (not_lt.mpr hn)]
  apply cauchySeq_sum_of_eventually_eq this
    (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)
  · exact C
  intro n
  simp only [v]
  split_ifs with H
  · rw [norm_zero]
    exact mul_nonneg hC (pow_nonneg hr₀.le _)
  · push Not at H
    exact h _ H

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

Goal state before:
pp: case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) 0

Tactic:
refine lt_of_le_of_ne (norm_nonneg _) ?_

Goal state after:
case convert_2
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) 0
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ PathConnectedSpace Y

Tactic:
rw [pathConnectedSpace_iff_univ, ← hf.range_eq]
  exact isPathConnected_range hf'

Goal state after: