mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
⊢ α ≃ᵐ β

Tactic:
by_cases h : Countable α

Goal state after:
case pos
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
⊢ α ≃ᵐ β

case neg
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : ¬Countable α
⊢ α ≃ᵐ β
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
⊢ α ≃ᵐ β

Tactic:
by_cases h : Countable α
  · letI := Countable.of_equiv α e
    refine ⟨e, ?_, ?_⟩ <;> apply measurable_of_countable
  refine measurableEquivOfNotCountable h ?_
  rwa [e.countable_iff] at h

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
    ← lintegral_add_left hf]
  simp only [Pi.add_apply]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
⊢ HasFiniteIntegral (fun x ↦ ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ∞

Tactic:
simp [hasFiniteIntegral_iff_norm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ

Tactic:
have h x : ‖(f x).toReal‖ₑ = .ofReal (f x).toReal := by
    rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ f x * g m x ≤ f x * g n x

Tactic:
h_mono_g hmn x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ f x * g n x ≤ f x * g n x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)

Goal state after:
case mpr.inl
y : ℝ
hy : 0 ≤ y
⊢ √(y * y) = y

case mpr.inr
x : ℝ
hx : x < 0
⊢ √x = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ^ 2 = max x 0

Tactic:
rcases lt_trichotomy x 0 with _ | _ | _ <;> grind [sqrt_eq_zero', sq_sqrt]

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

Goal state before:
pp: x : ℝ
⊢ √x ≤ 0 ↔ √x = 0

Tactic:
by simp [le_antisymm_iff, sqrt_nonneg]

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

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * (‖z‖ * ‖w‖)

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * (√(normSq z) * ‖w‖)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * (√(normSq z) * ‖w‖)

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * (√(normSq z) * √(normSq w))
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖-z‖ = ‖z‖

Tactic:
Complex.norm_def,

Goal state after:
z : ℂ
⊢ √(normSq (-z)) = ‖z‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ √(normSq (-z)) = ‖z‖

Tactic:
norm_def,

Goal state after:
z : ℂ
⊢ √(normSq (-z)) = √(normSq z)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z * w‖ = ‖z‖ * ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z * w)) = ‖z‖ * ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ √(normSq (z * w)) = ‖z‖ * ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z * w)) = √(normSq z) * ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ √(normSq (z * w)) = √(normSq z) * ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z * w)) = √(normSq z) * √(normSq w)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z / w‖ = ‖z‖ / ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z / w)) = ‖z‖ / ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ √(normSq (z / w)) = ‖z‖ / ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z / w)) = √(normSq z) / ‖w‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ √(normSq (z / w)) = √(normSq z) / ‖w‖

Tactic:
norm_def,

Goal state after:
z w : ℂ
⊢ √(normSq (z / w)) = √(normSq z) / √(normSq w)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℤ
hn : 0 ≤ n
⊢ ‖↑n‖ = ↑n

Tactic:
by
  rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]

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

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

Tactic:
norm_def,

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

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

Tactic:
norm_def,

Goal state after:
z : ℂ
⊢ |z.re| < √(normSq z) ↔ z.im ≠ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
x✝ : ℂ
⊢ (0 • x✝).re = re 0

Tactic:
simp [smul_re, smul_im]

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

Goal state before:
pp: case a
x✝ : ℂ
⊢ (0 • x✝).im = im 0

Tactic:
simp [smul_re, smul_im]

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

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).re = (n✝ • x✝ + x✝).re

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.re = ↑n✝ * x✝.re + x✝.re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).im = (n✝ • x✝ + x✝).im

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.im = ↑n✝ * x✝.im + x✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 • a✝).re = re 0

Tactic:
simp [smul_re, smul_im]

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 • a✝).im = im 0

Tactic:
simp [smul_re, smul_im]

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

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).re = (↑n✝ • a✝ + a✝).re

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.re = ↑n✝ * a✝.re + a✝.re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.im = ↑n✝ * a✝.im + a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).re = (-(↑n✝.succ • a✝)).re

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.re = -((↑n✝ + 1) * a✝.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).im = (-(↑n✝.succ • a✝)).im

Tactic:
simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.im = -((↑n✝ + 1) * a✝.im)
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 rw [mul_assoc]

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₂
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
dsimp only [norm]

Goal state after:
𝕜 : 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‖ * max ‖x.1‖ ‖x.2‖ ≤ max ‖(x⋆ * x).1‖ ‖(x⋆ * x).2‖
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
exact funext <| e.symm_apply_apply

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

Goal state before:
pp: case refine_1
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = I → f = AlgHom.id ℝ ℂ

Tactic:
refine fun h => algHom_ext ?_

Goal state after:
case refine_1
f : ℂ →ₐ[ℝ] ℂ
h : f I = I
⊢ f I = (AlgHom.id ℝ ℂ) I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case refine_2
f : ℂ →ₐ[ℝ] ℂ
⊢ f I = -I → f = ↑conjAe

Tactic:
refine fun h => algHom_ext ?_

Goal state after:
case refine_2
f : ℂ →ₐ[ℝ] ℂ
h : f I = -I
⊢ f I = ↑conjAe I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    ((algebraMap ℝ A) x₁ + y₁ • I') * ((algebraMap ℝ A) x₂ + y₂ • I')

Tactic:
rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I' +
      ((algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ -(starRingEnd K) I = I

Tactic:
conj_I,

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ - -I = I
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) ↑(re z) + (starRingEnd K) ↑(im z) * (starRingEnd K) I = ↑(re z) - ↑(im z) * I

Tactic:
conj_I,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (starRingEnd K) ↑(re z) + (starRingEnd K) ↑(im z) * -I = ↑(re z) - ↑(im z) * I
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ x.re = y ↔ x = ↑y

Tactic:
rw [← RCLike.re_eq_complex_re]

Goal state after:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ RCLike.re x = y ↔ x = ↑y
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = x.re ↔ ↑y = x

Tactic:
rw [← RCLike.re_eq_complex_re]

Goal state after:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = RCLike.re x ↔ ↑y = x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + (starRingEnd K) I * (starRingEnd K) z) / 2 = -(I * ((starRingEnd K) z - z) / 2)

Tactic:
conj_I,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = -(I * ((starRingEnd K) z - z) / 2)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ x.re ↔ 0 ≤ x

Tactic:
rw [← RCLike.re_eq_complex_re]

Goal state after:
x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ RCLike.re x ↔ 0 ≤ x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z / ‖z‖| ≤ 1

Tactic:
by
  rw [abs_div, abs_norm]
  exact div_le_one_of_le₀ (abs_im_le_norm _) (norm_nonneg _)

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
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ((starRingEnd 𝕜) z) =
      -(⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z

Tactic:
subst h''; exact h.conj_im_ax

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ pb,
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ pb,
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case succ
α : 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
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k
⊢ abv (f (k + max n i) + (∑ x ∈ range (k + max n i), f x + -∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + (∑ x ∈ range (k + max n i), a x + -∑ x ∈ range (max n i), a x)

Tactic:
simp only [sub_eq_add_neg] at hi

Goal state after:
case succ
α : 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
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ abv (f (k + max n i) + (∑ x ∈ range (k + max n i), f x + -∑ x ∈ range (max n i), f x)) ≤
    a (k + max n i) + (∑ x ∈ range (k + max n i), a x + -∑ x ∈ range (max n i), a x)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
hc : 0 < c
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hx : f x ≠ 0
hc : 0 < c
hle : (c * ‖g x‖)⁻¹ ≤ ‖f x‖⁻¹
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul,
        ← div_div, mul_div_assoc, mul_div_right_comm, Complex.norm_mul, Complex.norm_div,
        norm_natCast]
      gcongr
      exact le_trans hm (Nat.le_succ _)

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
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * ((↑n.factorial)⁻¹ * ((↑n.succ - 1)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ))) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
← mul_assoc (n.factorial⁻¹ : α),

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

Goal state before:
pp: x : ℂ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]

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

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

Tactic:
simp [exp_ofReal_re, sin_ofReal_re]

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ cexp (z * I) ^ n = cexp (↑n * z * I)

Tactic:
← exp_nat_mul,

Goal state after:
n : ℕ
z : ℂ
⊢ cexp (↑n * (z * I)) = cexp (↑n * z * I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)

Tactic:
simp [cosh_sq]

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

Goal state before:
pp: x : ℝ
⊢ tanh x < 1

Tactic:
by
  rw [tanh_eq]
  field_simp
  grind [exp_pos]

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

Goal state before:
pp: x : ℝ
⊢ -1 < tanh x

Tactic:
by
  rw [tanh_eq]
  field_simp
  grind [exp_pos]

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

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ 0 ≤ |x| ^ n / ↑n.factorial

Tactic:
simp [div_nonneg, abs_nonneg]

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n * ↑n)) = rexp (-t)

Tactic:
div_mul_cancel₀

Goal state after:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-t) = rexp (-t)

case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

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

Tactic:
convert! continuous_exp.tendsto 0

Goal state after:
⊢ 1 = rexp 0
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ ‖↑x‖ = infDist x ↑S

Tactic:
by
  rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.divLeft x).isometry,
    ← IsometryEquiv.preimage_symm]
  simp

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
⊢ ∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt

Tactic:
rintro z ⟨x, hx, y, hy, rfl⟩

Goal state after:
E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ x ∈ t, ‖x‖ ≤ Rt
x : E
hx : x ∈ s
y : E
hy : y ∈ t
⊢ ‖(fun x1 x2 ↦ x1 * x2) x y‖ ≤ Rs + Rt
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ / {y} = ball (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior ∅ = ∅

Tactic:
interior_empty

Goal state after:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ ∅ = ∅
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝¹ : r ≠ 0
hr✝ : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r

pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)

Tactic:
· exact hr

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by
  rw [← cos_pi_div_two_sub, ← cos_pi_div_three]
  congr
  ring

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ x * r) '' Ioo a b = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
image_mul_right_Ioo _ _ hr

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)
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
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1

Tactic:
rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]

Goal state after: