mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ

pp: case hr
α : 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)
⊢ 2 ≠ ∞

Tactic:
]

Goal state after:
case hr
α : 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)
⊢ 2 ≠ ∞
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ ↑(nndist z w) = ↑(nndist z.im w.im)

Tactic:
nndist_of_re_eq h

Goal state after:
z w : ℂ
h : z.re = w.re
⊢ ↑(nndist z.im w.im) = ↑(nndist z.im w.im)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.re = w.re
⊢ ↑(nndist z.im w.im) = ↑(nndist z.im w.im)

Tactic:
]

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

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

Tactic:
]

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
x : α
hx : f x < ∞
h'x : f x = AEMeasurable.mk f hf x
⊢ f x < ∞

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x < ∞
h'x : f x = AEMeasurable.mk f hf x
⊢ f x < ∞
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ ↑(nndist z.re w.re) = ↑(nndist z.re w.re)

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ 2 * |z.im| = 2 * |z.im|

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ 2 * Real.nnabs z.im = 2 * Real.nnabs z.im

Tactic:
]

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, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
]

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, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
]

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 μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
]

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 * fun i ↦ (f i)⁻¹) ≤ μ

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ
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
⊢ μ ≤ μ

Tactic:
]

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 * fun i ↦ (f i)⁻¹) = μ

Tactic:
]

Goal state after:
α : 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 * fun i ↦ (f i)⁻¹) = μ
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 μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

pp: case hr
α : 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 μ
⊢ ‖c‖ₑ ≠ ∞

Tactic:
]

Goal state after:
α : 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 μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

case hr
α : 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 μ
⊢ ‖c‖ₑ ≠ ∞
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
⊢ μ = μ

Tactic:
]

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 ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqRe f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).re
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
]

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqIm f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).im
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 μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

pp: case hr
α : 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 μ
⊢ ‖c‖ₑ ≠ ∞

Tactic:
]

Goal state after:
α : 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 μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

case hr
α : 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 μ
⊢ ‖c‖ₑ ≠ ∞
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
s : Set α
hs : MeasurableSet s
hμs : μ {a | ¬s.indicator f a = 0 a} = 0
⊢ μ s = 0

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : μ {a | ¬s.indicator f a = 0 a} = 0
⊢ μ s = 0
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
]

Goal state after:
z : ℂ
hz : z.re * z.re + z.im * z.im = 1
⊢ z.im * z.im = 1 - z.re * z.re
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ ∫⁻ (a : α) in spanningSets μ n ∩ f ⁻¹' Iic ↑n, ↑(f a) ∂μ < ∞

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ ∫⁻ (a : α) in spanningSets μ n ∩ f ⁻¹' Iic ↑n, ↑(f a) ∂μ < ∞
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
]

Goal state after:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (-↑x + I * ↑√(1 - x ^ 2)) = 1
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ∀ (x : α), ∃ i, x ∈ spanningSets μ i ∩ f ⁻¹' Iic ↑i

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ∀ (x : α), ∃ i, x ∈ spanningSets μ i ∩ f ⁻¹' Iic ↑i
Module: Mathlib.Analysis.Complex.Order

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

Tactic:
]

Goal state after:
z w : ℂ
⊢ (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ 0 ≤ (z * z).re ∧ 0 = (z * z).im ↔ z.im = 0

Tactic:
mul_re,

Goal state after:
z : ℂ
⊢ 0 ≤ z.re * z.re - z.im * z.im ∧ 0 = (z * z).im ↔ z.im = 0
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:
]

Goal state after:
z : ℂ
⊢ 0 ≤ z.re ^ 2 - z.im ^ 2 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.im = 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ (z * z).re ≤ 0 ∧ (z * z).im = 0 ↔ z.re = 0

Tactic:
mul_re,

Goal state after:
z : ℂ
⊢ z.re * z.re - z.im * z.im ≤ 0 ∧ (z * z).im = 0 ↔ z.re = 0
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:
]

Goal state after:
z : ℂ
⊢ z.re ^ 2 - z.im ^ 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.re = 0
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 ≠ ∞
this : f =ᵐ[μ] fun x ↦ ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x).toNNReal)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᵐ[μ] fun x ↦ ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x).toNNReal)
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:
]

Goal state after:
α : 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₂
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:
]

Goal state after:
α : 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₂
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:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ ↑q * a < ↑q * b
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:
]

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ ↑q * a < ↑q * b
Module: Mathlib.Analysis.Complex.Order

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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.re

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0

Tactic:
]

Goal state after:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ z ≤ 0 ↔ z ≤ 0

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ], IsFiniteMeasure μ → SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite (sum fun n ↦ (sfiniteSeq μ n).withDensity f)

Tactic:
]

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ], IsFiniteMeasure μ → SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ SFinite (sum fun n ↦ (sfiniteSeq μ n).withDensity f)
Module: Mathlib.Data.Complex.Basic

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

Tactic:
]

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

Goal state before:
pp: x y : ℝ
⊢ x * x + y * y = x * x + y * y

Tactic:
]

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) + μ.withDensity (∑' (n : ℕ), s.indicator 1)

Tactic:
]

Goal state after:
α : 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) + μ.withDensity (∑' (n : ℕ), s.indicator 1)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ -1 = -1

Tactic:
]

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

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

Tactic:
]

Goal state after:
case e_a.e_f
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
x : α
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
Module: Mathlib.Data.Complex.Basic

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

Tactic:
]

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

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
z w : ℂ
⊢ normSq z + normSq (-w) + 2 * (z * (starRingEnd ℂ) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
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 ((μ.restrict s).withDensity 1)

Tactic:
]

Goal state after:
α : 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 ((μ.restrict s).withDensity 1)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ↑0 = ↑0

Tactic:
]

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

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

Tactic:
]

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))
this : SigmaFinite (μ.withDensity (s.indicator 1))
⊢ SFinite (μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1))

Tactic:
]

Goal state after:
α : 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))
this : SigmaFinite (μ.withDensity (s.indicator 1))
⊢ SFinite (μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1))
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 (μ.withDensity fun x ↦ c • 1)

Tactic:
]

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

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

Tactic:
by simp [NNRat.smul_def]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)
Module: Mathlib.Data.Complex.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
n : ℕ
h : n = 0
⊢ n = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
]

Goal state after:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.Data.Complex.Basic

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

Tactic:
]

Goal state after:
a₁ a₂ b : ℝ
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}