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

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
⊢ Disjoint (Function.support g) (Function.support h) →
    Measurable g →
      Measurable h →
        ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
          ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
            ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
_

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝ : Disjoint (Function.support g) (Function.support h)
⊢ Measurable g →
    Measurable h →
      ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
        ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
          ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
⊢ Measurable h →
    ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
      ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
        ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
_

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
a✝ : Measurable h
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
    ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
      ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
a✝ : α
htendsto : Tendsto (fun n ↦ f n a✝) atTop (𝓝 (g a✝))
⊢ a✝ ∈ univ → Tendsto (fun n ↦ f n a✝) atTop (𝓝 (g a✝))

Tactic:
_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
a✝¹ : α
htendsto : Tendsto (fun n ↦ f n a✝¹) atTop (𝓝 (g a✝¹))
a✝ : a✝¹ ∈ univ
⊢ Tendsto (fun n ↦ f n a✝¹) atTop (𝓝 (g a✝¹))
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:

Tactic:
(∫⁻ a, ‖f' a‖ₑ ∂μ) ≤ ∫⁻ a, bound' a ∂μ :=
      lintegral_mono_ae <| ae_enorm_le_bound h_bound h_lim
    _ < ∞ := bound_hasFiniteIntegral

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

Goal state before:
pp: x : ℝ
⊢ 1 ≤ √x ↔ 1 ≤ x

Tactic:
by
  rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]

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

Goal state before:
pp: x : ℝ
⊢ √x ≤ 1 ↔ x ≤ 1

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]

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

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

Tactic:
by
  rw [sq, sq, dist_eq]
  rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖min (f x) 0‖ ≤ ‖f x‖

Tactic:
by simpa [abs_le] using neg_abs_le _

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

Goal state before:
pp: s t : Set ℝ
⊢ (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
simp [Set.Nonempty, reProdIm, Complex.exists]

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 φ
⊢ ∫⁻ (z : G × G), φ (z.1 * z.2) ∂(μ.withDensity f).prod (μ.withDensity g) = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
prod_withDensity₀ hf hg,

Goal state after:
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 φ
⊢ (∫⁻ (z : G × G), φ (z.1 * z.2) ∂(μ.prod μ).withDensity fun z ↦ f z.1 * g z.2) =
    ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
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₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * ‖f v‖ ≤ ‖g‖ * (‖f‖ * ‖v‖)

Tactic:
by gcongr; apply le_opNorm

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 ↔ a * star a = b * star b

Tactic:
simpa [← mul_inv_rev] using mul_inv_mem_iff a⁻¹ b⁻¹

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

Goal state before:
pp: x : ℝ
⊢ -↑x ∈ slitPlane ↔ x < 0

Tactic:
by
  simpa using ofReal_mem_slitPlane (x := -x)

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ star x * x = ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x) + I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x))

Tactic:
conv_lhs => rw [← realPart_add_I_smul_imaginaryPart x]
    simp [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, smul_smul, smul_sub]
    grind

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ re ↑q = ↑q

Tactic:
by rw [← ofReal_nnratCast, ofReal_re]

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

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
rw [domRestrict_eq, toFun_eq_coe e, e.injOn.injective_iff e.source (by simp)]
    exact Subtype.val_injective

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < z⁻¹

Tactic:
rw [← hx', ← ofReal_inv, ofReal_pos]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : ↑x = z
⊢ 0 < x⁻¹
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
← ha2,

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
x : K
⊢ ↑(re x) = x

Tactic:
nth_rw 2 [← re_add_im x]; simp [h]

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:
subst h''; exact h.re

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
c₁ : E''
c₂ : F''
⊢ ((fun x ↦ c₁) =Θ[l] fun x ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Tactic:
by
  simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm

Goal state after:
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:
by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_neg_right

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 : α) in l, g x = 0 → f x = 0

pp: case a
α : 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
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
· apply (Filter.Tendsto.eventually_ge_atTop h 1).mono
    intro x h h0
    simp only [h0, zero_div] at h
    grind

Goal state after:
case a
α : 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
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h : x ≤ 0
⊢ 0 < rexp x

Tactic:
rw [← neg_neg x, Real.exp_neg]
    exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

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

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

Tactic:
by
  have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
  convert exp_bound hxc hn <;>
  norm_cast

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
⊢ Summable fun n ↦ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Tactic:
refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 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, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
have C₁_mem : C₁ ∈ ubounds := by
    rw [Set.mem_ofPred]
    intro m hm
    calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)

Goal state after:
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
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun a ↦ a + d) ∘ fun x ↦ n • id x) m ≡ d [MOD n]

Tactic:
by simp [Nat.modEq_iff_dvd]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ IsBigOWith (sSup (Norm.norm '' f '' s) / ‖c‖) (𝓟 s) f fun x ↦ c

Tactic:
rw [isBigOWith_principal, div_mul_cancel₀ _ hc]
  exact fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
   |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
   |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
⊢ x ∈ {x | x.re ≤ a} → ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
_

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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
⊢ ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
⊢ n ≥ 0 → |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

Tactic:
_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
⊢ n ≥ 0 → (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ C * x ^ n ≤ rexp x

Tactic:
← le_div_iff₀' hC₀

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ rexp x / C
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 : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ

Tactic:
exact add_le_add (Nat.zero_le _) (by simp)

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

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)

Tactic:
apply sin_nonneg_of_nonneg_of_le_pi

Goal state after:
case h0x
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ x / 2

case hxp
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ x / 2 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (range sin).Infinite

Tactic:
Real.range_sin

Goal state after:
⊢ (Icc (-1) 1).Infinite
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
x : E
r : ℝ
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩
  obtain ⟨y, hy⟩ := exists_norm_eq E hr
  exact ⟨x + y, by simpa using hy⟩

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

Goal state before:
pp: r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n ↦ ↑n * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr

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

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

Tactic:
simp only [hz, add_neg_cancel_left]

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

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)

Tactic:
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

Tactic:
rw [eventually_atTop] at h
    rcases h with ⟨N, hN⟩
    rw [← @summable_nat_add_iff α _ _ _ _ N]
    refine .of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n)
      (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun n ↦ ?_
    conv_rhs => rw [mul_comm, ← zero_add N]
    refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_
    convert! hN (i + N) (N.le_add_left i) using 3
    ac_rfl

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

Goal state before:
pp: case right
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩

Goal state after:
case right
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ ContinuousOn f (range ⇑⋯.somePath)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ IsPathConnected F ↔ IsPathConnected (f '' F)

Tactic:
by
  simp only [IsPathConnected, forall_mem_image, exists_mem_image]
  refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_
  rw [hf.joinedIn_image hx hy]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
a✝ : ℕ
⊢ ‖f (a✝ + 1)‖ / ‖f a✝‖ ≤ r → f a✝ ≠ 0 → ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖

Tactic:
_

Goal state after:
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
a✝¹ : ℕ
a✝ : ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖ ≤ r
⊢ f a✝¹ ≠ 0 → ‖f (a✝¹ + 1)‖ ≤ r * ‖f a✝¹‖
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
s : Set X
⊢ ⇑(coev X Y y) '' s = {y} ×ˢ s

Tactic:
by simp [singleton_prod]

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

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a✝ : ℕ
⊢ r ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖ → ‖f a✝‖ ≠ 0 → r * ‖f a✝‖ ≤ ‖f (a✝ + 1)‖

Tactic:
_

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
⊢ ‖f a✝¹‖ ≠ 0 → r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C

Tactic:
enter [n]

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n * w ^ n‖ ≤ C
Module: Mathlib.Topology.Path

Goal state before:
pp: ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
⊢ (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i ↦ (γ₀ i).trans (γ₁ i)

Tactic:
by
  ext t i
  unfold Path.trans
  simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
  split_ifs
  · rfl
  · rfl

Goal state after: