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

Goal state before:
pp: case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
U : Set α
hU : IsOpen[inst✝²] U
⊢ ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε

Tactic:
ε

Goal state after:
case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
U : Set α
hU : IsOpen[inst✝²] U
ε : ℝ≥0∞
⊢ ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
⊢ ∀ (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ ⋃ i, s i,
        ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Tactic:
ε

Goal state after:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
⊢ ε ≠ 0 →
    ∃ F ⊆ ⋃ i, s i,
      ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) (Prod.map f g ⁻¹' s ×ˢ t) =
    (sfiniteSeq μa i.1) (f ⁻¹' s) * (sfiniteSeq μc i.2) (g ⁻¹' t)

Tactic:
exact prod_prod (f ⁻¹' s) (g ⁻¹' t)

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
⊢ map (fun x ↦ x * g) (comap (⇑f) μ) = comap (⇑f) μ

Tactic:
by
    ext s hs
    rw [map_apply (by fun_prop) hs]
    repeat rw [hf.comap_apply]
    have : f '' (· * g) ⁻¹' s = (· * f g) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨y * g, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩
    rw [this, ← map_apply (by fun_prop), IsMulRightInvariant.map_mul_right_eq_self]
    exact hf.measurableSet_image.mpr hs

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
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ s⁻¹ = 0 ↔ μ s = 0

Tactic:
refine ⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ (μ.withDensity f) s = 0

Tactic:
withDensity_apply _ hs₁

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs₁ : MeasurableSet s
hs₂ : μ s = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0
Module: Mathlib.MeasureTheory.Function.Egorov

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

Tactic:
refine le_trans (measure_iUnion_le _) (le_trans
    (ENNReal.tsum_le_tsum <| notConvergentSeqLTIndex_spec (half_pos hε) hf hsm hs hfg) ?_)

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = √↑x

Tactic:
rw [Real.sqrt, Real.toNNReal_coe]

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

Goal state before:
pp: case inr
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact sqrt_le_sqrt_iff hy

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

Goal state before:
pp: ι : Type u_2
f g : ι → ℝ
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
⊢ ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Tactic:
by
  simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))

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

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im

Tactic:
dist_eq_re_im,

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

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re

Tactic:
dist_eq_re_im,

Goal state after:
z w : ℂ
h : z.im = w.im
⊢ √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2) = dist z.re w.re
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
this : c • μ = c • 1 • μ
⊢ SFinite (c • μ)

Tactic:
rw [this, ← smul_assoc, ← withDensity_const]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
this : c • μ = c • 1 • μ
⊢ SFinite (μ.withDensity fun x ↦ c • 1)
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : 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)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
by
  obtain rfl | hs_nonempty := s.eq_empty_or_nonempty
  · simp [h_zero]
  · exact le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs

Goal state after:
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₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖n • f v‖ ≤ n • b * ‖v‖

Tactic:
nsmul_eq_mul,

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₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖n • f v‖ ≤ ↑n * b * ‖v‖
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
a : ℝ
b : ↥(skewAdjoint A)
⊢ ⟨-I • ↑(a • b), ⋯⟩ = (RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩

Tactic:
by ext; simp [smul_comm I]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ f =Θ[l] g

Tactic:
refine ⟨isBigO_of_div_tendsto_nhds_of_ne_zero h hc,
    isBigO_of_div_tendsto_nhds_of_ne_zero ?_ (inv_ne_zero hc)⟩
  convert! h.inv₀ hc using 1
  ext
  simp

Goal state after:
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
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Tactic:
simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
⊢ IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Tactic:
ε

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
⊢ ε > 0 → ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z / ↑m.succ‖ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
Complex.norm_div,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ‖↑m.succ‖ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * ((↑(m.choose I))⁻¹ * ↑(m.choose I))))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
rw [inv_mul_cancel₀ h₁]

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
by_cases hgx : g x = 0

Goal state after:
case pos
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

case neg
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : ¬g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * ‖x ^ (x_1 - n) / ↑x_1.factorial‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
Complex.norm_div,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ‖↑x_1.factorial‖) ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ Ico n j, ‖x‖ ^ n * ‖x ^ (x_1 - n) / ↑x_1.factorial‖ ≤
    ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
Complex.norm_div,

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ Ico n j, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ‖↑x_1.factorial‖) ≤
    ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / ↑(m - n).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Tactic:
exact forall₂_congr fun c _hc => e.isBigOWith_congr

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

Goal state before:

Tactic:
‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖ := by nth_rw 1 [hy_eq]
    _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * ‖y - x‖ ^ 2 := h_sq (y - x) (hyx.le.trans hr_le)
    _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) := by grw [hyx_sq_le]
    _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring

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

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

Tactic:
intro b'

Goal state after:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' : ℝ
⊢ ∀ (e : ℝ), 0 < b' → Tendsto (fun x ↦ x ^ n / (b' * rexp x + e)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 2 / 2 ≤ π / 2

Tactic:
by rw [div_self two_ne_zero]; exact one_le_pi_div_two

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ π
⊢ |sin x| = sin |x|

Tactic:
rcases lt_or_ge x 0 with h | h
  · rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]
  · rw [abs_of_nonneg h, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi h (abs_le.1 hx).2)]

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
this : Function.Surjective fun x ↦ c • x
y : E
⊢ ⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y) = ⨅ (_ : y ∈ s), ‖c‖₊ • edist x y

Tactic:
smul_mem_smul_set_iff₀ hc,

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
this : Function.Surjective fun x ↦ c • x
y : E
⊢ ⨅ (_ : y ∈ s), edist (c • x) (c • y) = ⨅ (_ : y ∈ s), ‖c‖₊ • edist x y
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 < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
by
      rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
⊢ Summable fun n ↦ ↑n ^ k * r ^ n

Tactic:
obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable fun n ↦ ↑n ^ k * r ^ n
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : C(X, Y)
hf : Tendsto F l (𝓝 f)
s : Set X
a✝ : IsCompact s
⊢ ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

Tactic:
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
let := pathSetoid X
  constructor
  · intro h
    refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
    rintro ⟨x⟩ ⟨y⟩
    exact Quotient.sound (PathConnectedSpace.joined x y)
  · unfold ZerothHomotopy
    rintro ⟨h, h'⟩
    exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩

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

Goal state before:
pp: ⊢ IsDiscrete ↑(AddSubgroup.zmultiples 1)

Tactic:
SetLike.isDiscrete_iff_discreteTopology

Goal state after:
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: a : ℝ
ha : a ≠ 0
⊢ IsDiscrete ↑(AddSubgroup.zmultiples a)

Tactic:
SetLike.isDiscrete_iff_discreteTopology

Goal state after:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: a : ℝ
ha : a ≠ 0
⊢ Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (cocompact ℝ)

Tactic:
by
  apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha
  rw [AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology]
  infer_instance

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

Goal state before:
pp: a : ℝ
⊢ IsDiscrete ↑(zmultiples a)

Tactic:
SetLike.isDiscrete_iff_discreteTopology

Goal state after:
a : ℝ
⊢ DiscreteTopology ↥(zmultiples a)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
⊢ x = y

Tactic:
have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
this : 0 < ↑N
⊢ x = y
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑1
h₂ : ↑1 ≤ t₁
⊢ γ.extend ↑1 = γ.extend t₁

Tactic:
simp [γ.extend_of_one_le h₂]

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ addOrderOf u • (p * (↑n / ↑(addOrderOf u)))

Tactic:
nsmul_eq_mul,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ ↑(addOrderOf u) * (p * (↑n / ↑(addOrderOf u)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0

Tactic:
by
  rw [arccos, arcsin_of_one_le hx, sub_self]

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

Goal state before:
pp: case inl
⊢ log (0 / 0) = 0

Tactic:
simp [*]

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ log (x / x) = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
⊢ (0 / 0).arg = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
x : ℂ
hx : x ≠ 0
⊢ (x / x).arg = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ z.arg = Real.arccos (z.re / ‖z‖)

Tactic:
rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ ↑x.re + (↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I) =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
← add_sub_assoc

Goal state after:
x : ℂ
⊢ ↑x.re + ↑x.im * I - ↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) ≤ log (1 + x)

Tactic:
le_log_iff_exp_le (by grind)

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ rexp (2 * x / (x + 2)) ≤ 1 + x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < log (1 + x)

Tactic:
lt_log_iff_exp_lt (by grind)

Goal state after:
x : ℝ
hx : 0 < x
⊢ rexp (2 * x / (x + 2)) < 1 + x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
obtain ⟨n, hn⟩ := exp_eq_exp_iff_exists_int.1 h
  simp [hn]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ 1 ^ x = 1

Tactic:
rw [cpow_def]
  split_ifs <;> simp_all [one_ne_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h✝ : x.arg = π
⊢ |π| = |x.arg|

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h✝ : ¬x.arg = π
⊢ |(-x.arg)| = |x.arg|

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.im < ‖z‖

pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Tactic:
←
      abs_of_nonneg him,

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ |z.im| < ‖z‖

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]

Goal state after: