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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
⊢ (fun x ↦ (f x)⁻¹ * i x) ≤ g

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ 1 + x + (x / 2) ^ 2 = (1 + x / 2) ^ 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ √(1 + x) ≤ 1 + x / 2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = ∏ i ∈ s, √(x i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
s : Finset ι
f g : ι → ℝ
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ 0 ≤ f x✝¹ ^ 2

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ |z.re| ≤ ‖z‖

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖(starRingEnd ℂ) z‖ = ‖z‖

Tactic:
by

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

Goal state before:
pp: ⊢ ‖I‖ = 1

Tactic:
by

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

Goal state before:
pp: ⊢ ‖I‖₊ = 1

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖ = ‖r‖

Tactic:
simp [norm_def, Real.sqrt_mul_self_eq_abs]

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

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖ = ‖r‖

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖₊ = ‖r‖₊

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖ = |↑n|

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ normSq z = ‖z‖ ^ 2

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ 1 < normSq x ↔ 1 < ‖x‖

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ 1 ≤ normSq x ↔ 1 ≤ ‖x‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(x ^ 2 + y ^ 2)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ici 0
⊢ normSq ↑√x = x

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ |z.re| + |z.im|

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
⊢ 0 ≤ m

Tactic:
by

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

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'

Tactic:
by

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

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(m ^ 2 + m ^ 2) = √2 * m

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
by

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

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

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

Tactic:
by

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:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * |z.im|

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ↑(nndist ((starRingEnd ℂ) z) z) = ↑(2 * Real.nnabs z.im)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ dist z ((starRingEnd ℂ) z) = 2 * |z.im|

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ (↑f n).re) j - (fun n ↦ (↑f n).re) i| ≤ ‖↑f j - ↑f i‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ (↑f n).im) j - (fun n ↦ (↑f n).im) i| < ε

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).withDensity f⁻¹ ≤ μ

Tactic:
by

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

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
⊢ (fun x ↦ ‖x‖) (↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j) < ε

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
this : IsAbsoluteValue fun x ↦ ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x ↦ ‖x‖) (limAux f)) x✝).re = (↑(const (fun x ↦ ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).re

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) = μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
by

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

Goal state before:
pp: p : ℂ → Prop
⊢ (∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }

Tactic:
by

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

Goal state before:
pp: p : ℂ → Prop
⊢ (∃ x, p x) ↔ ∃ a b, p { re := a, im := b }

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
this : IsAbsoluteValue fun x ↦ ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x ↦ ‖x‖) (limAux f)) x✝).im = (↑(const (fun x ↦ ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).im

Tactic:
by

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

Goal state before:
pp: z w : ℝ
⊢ z = w → ↑z = ↑w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
by

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

Goal state before:
pp: r s : ℝ
⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun x ↦ (f x)⁻¹) = μ

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqRe f).lim = f.lim.re

Tactic:
by

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

Goal state before:
pp: r s : ℝ
⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im

Tactic:
by

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

Goal state before:
pp: r : ℝ
z : ℂ
⊢ (↑r * z).re = r * z.re

Tactic:
by

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

Goal state before:
pp: r : ℝ
z : ℂ
⊢ (↑r * z).im = r * z.im

Tactic:
by

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

Goal state before:
pp: z : ℂ
r : ℝ
⊢ (z * ↑r).re = z.re * r

Tactic:
by

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

Goal state before:
pp: z : ℂ
r : ℝ
⊢ (z * ↑r).im = z.im * r

Tactic:
by

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

Goal state before:
pp: ⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqIm f).lim = f.lim.im

Tactic:
by

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

Goal state before:
pp: a b : ℝ
⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (↑z.re + ↑z.im * I).re = z.re ∧ (↑z.re + ↑z.im * I).im = z.im

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (z * I).re = -z.im

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (z * I).im = z.re

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = -z.im

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (I * z).im = z.re

Tactic:
by

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

Goal state before:
pp: p : ℝ × ℝ
⊢ equivRealProd.symm p = ↑p.1 + ↑p.2 * I

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : ℂ), equivRealProd.toFun (x + y) = equivRealProd.toFun x + equivRealProd.toFun y

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ (fun x ↦ ‖x‖) ((fun n ↦ (starRingEnd ℂ) (↑f n)) j - (fun n ↦ (starRingEnd ℂ) (↑f n)) i) < ε

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqConj f).lim.re = ((starRingEnd ℂ) f.lim).re

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqConj f).lim.im = ((starRingEnd ℂ) f.lim).im

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : ℂ), 0 + a = a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : ℂ), a + 0 = a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ℂ), 0 • x = 0

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ z.im * z.im = 1 - z.re * z.re

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
⊢ μ ≪ μ.withDensity f

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ ‖z - 1‖ ^ 2 = 2 * (1 - z.re)

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z ∈ Metric.sphere 0 1
⊢ ‖z‖ = 1

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (n : ℕ) (x : ℂ), (n + 1) • x = n • x + x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : ℂ), 0 • a = 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (↑x + I * ↑√(1 - x ^ 2)) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖-x‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (↑x - I * ↑√(1 - x ^ 2)) = 1

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (n : ℕ) (a : ℂ), ↑n.succ • a = ↑n • a + a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ^ 2 - z.im ^ 2 ∧ (z.re = 0 ∨ z.im = 0) → z.im = 0

Tactic:
by

Goal state after: