mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Order

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z ^ 2 ↔ z.im = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
inst✝¹ : ENorm ε
inst✝ : MeasurableSingletonClass α
f : α → ε
⊢ HasFiniteIntegral f Measure.count ↔ ∑' (x : α), ‖f x‖ₑ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ HasFiniteIntegral f Measure.count ↔ Summable fun x ↦ ‖f x‖

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ z ^ 2 ≤ 0 ↔ z.re = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ _q • _a₁ ≤ _q • _a₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ _q • _a₁ < _q • _a₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
⊢ |q • a| = q • |a|

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
by

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

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ SigmaFinite (μ.withDensity f)

Tactic:
by

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

Goal state before:
pp: x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
by

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

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Tactic:
by

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

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)

Tactic:
by

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

Goal state before:
pp: r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
by

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

Goal state before:
pp: z : ℂ
this : 0 ≤ ‖z‖
x✝ : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
⊢ z.re = ‖z‖

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ z.re = -‖z‖ ↔ z ≤ 0

Tactic:
by

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

Goal state before:
pp: ⊢ Monotone ofReal

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ ↑x ≠ 0

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.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), 1 * a = a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : ℂ), a * 1 = 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.Data.Complex.Basic

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
by

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

Goal state before:
pp: n : ℤ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
by

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

Goal state before:
pp: x : ℂ
⊢ (fun z ↦ { re := z.re, im := -z.im }) ((fun z ↦ { re := z.re, im := -z.im }) x) = x

Tactic:
by

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

Goal state before:
pp: a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im } = { re := b.re, im := -b.im } * { re := a.re, im := -a.im }

Tactic:
by

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

Goal state before:
pp: a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im } = { re := a.re, im := -a.im } + { re := b.re, im := -b.im }

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ((starRingEnd ℂ) I).re = (-I).re ∧ ((starRingEnd ℂ) I).im = (-I).im

Tactic:
by

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

Goal state before:
pp: ⊢ (starRingEnd ℂ) (-I) = I

Tactic:
by

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

Goal state before:
pp: z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ (starRingEnd ℂ) z = z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f)

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ (∃ r, z = ↑r) → ↑z.re = z

Tactic:
by

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

Goal state before:
pp: ⊢ re 0 * re 0 + im 0 * im 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ ∀ (i : ℕ), Measurable (s.indicator 1)

Tactic:
by

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

Goal state before:
pp: r : ℝ
⊢ normSq ↑r = r * r

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ normSq { re := x, im := y } = x ^ 2 + y ^ 2

Tactic:
normSq_mk,

Goal state after:
x y : ℝ
⊢ x * x + y * y = x ^ 2 + y ^ 2
Module: Mathlib.Data.Complex.Basic

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ↑(normSq z) = (starRingEnd ℂ) z * z

Tactic:
by

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

Goal state before:
pp: ⊢ normSq 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ normSq 1 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ normSq I = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ I ^ 2 = -1

Tactic:
by

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

Goal state before:
pp: ⊢ I ^ 3 = -I

Tactic:
by

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

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
by

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

Goal state before:
pp: ⊢ I ^ 4 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ I ^ n = I ^ (n % 4)

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 : ℝ
n : ℕ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.re = z.re / normSq z

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.im = -z.im / normSq z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))

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.Data.Complex.Basic

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite (μ.withDensity (s.indicator 1))

Tactic:
by

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

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: z w : ℂ
⊢ (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ SFinite (μ.withDensity f)

Tactic:
by

Goal state after:
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
⊢ c • μ = c • 1 • μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℚ≥0
z : ℂ
⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im

Tactic:
by

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

Goal state before:
pp: α : Type u_1
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℚ
z : ℂ
⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im

Tactic:
by

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

Goal state before:
pp: q : ℚ≥0
r : ℝ
⊢ ↑(q • r) = q • ↑r

Tactic:
by

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

Goal state before:
pp: q : ℚ
r : ℝ
⊢ ↑(q • r) = q • ↑r

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ I⁻¹ = -I

Tactic:
by

Goal state after:
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
⊢ SFinite (c • μ)

Tactic:
by

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

Goal state before:
pp: m : ℤ
⊢ I ^ m = I ^ (m % 4)

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ normSq z⁻¹ = (normSq z)⁻¹

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }

Tactic:
by

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

Goal state before:
pp: z : ℂ
x : ℝ
⊢ (z / ↑x).re = z.re / x

Tactic:
by

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

Goal state before:
pp: z : ℂ
x : ℝ
⊢ (z / ↑x).im = z.im / x

Tactic:
by

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

Goal state before:
pp: z : ℂ
n : ℕ
⊢ (z / ↑n).re = z.re / ↑n

Tactic:
by

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

Goal state before:
pp: z : ℂ
n : ℕ
⊢ (z / ↑n).im = z.im / ↑n

Tactic:
by

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

Goal state before:
pp: z : ℂ
n : ℤ
⊢ (z / ↑n).re = z.re / ↑n

Tactic:
by

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

Goal state before:
pp: z : ℂ
n : ℤ
⊢ (z / ↑n).im = z.im / ↑n

Tactic:
by

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

Goal state before:
pp: z : ℂ
x : ℚ
⊢ (z / ↑x).re = z.re / ↑x

Tactic:
by

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

Goal state before:
pp: z : ℂ
x : ℚ
⊢ (z / ↑x).im = z.im / ↑x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite μ

Tactic:
by

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

Goal state before:
pp: z : ℂ
⊢ ↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)

Tactic:
by

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

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
by

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

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s t : Set ℝ
⊢ s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
⊢ SFinite μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
⊢ SFinite μ

Tactic:
by
  obtain ⟨s, h⟩ := exists_sum_smul_dirac μ
  rw [h]
  infer_instance

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

Goal state before:
pp: a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ (fun x_1 ↦ ↑x_1 + ↑(equivRealProd x).2 * I) x.re = x

Tactic:
by

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

Goal state before:
pp: a₁ a₂ b : ℝ
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b}

Tactic:
by

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

Goal state before:
pp: b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ (fun y ↦ ↑x.re + ↑y * I) x.im = x

Tactic:
by

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

Goal state before:
pp: a b₁ b₂ : ℝ
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun z ↦ f z.1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, f i ≤ 0
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f g : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hfg : ∀ i ∈ s, f i ≤ g i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ ↑(#s) • a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ ↑(#s) • a ≤ ∑ i ∈ s, (fun i ↦ f i) i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
⊢ μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun z ↦ g z.2

Tactic:
by

Goal state after: