mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

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 m x ≤ f x * g n x
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hx : f x ≠ ∞
⊢ ENNReal.ofReal (f x).toReal = f x

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hx : f x ≠ ∞
⊢ ENNReal.ofReal (f x).toReal = f x
Module: Mathlib.MeasureTheory.Function.Egorov

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

Tactic:
;

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

Goal state before:
pp: x y : ℝ≥0
⊢ x * y ≤ max x y * max x y

Tactic:
;

Goal state after:
x y : ℝ≥0
⊢ x * y ≤ max x y * max x y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ Continuous fun x ↦ ↑(NNReal.sqrt x.toNNReal)

Tactic:
;

Goal state after:
⊢ Continuous fun x ↦ ↑(NNReal.sqrt x.toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ NNReal.sqrt x.toNNReal ≤ NNReal.sqrt y.toNNReal ↔ x ≤ y

Tactic:
NNReal.sqrt_le_sqrt,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ x.toNNReal ≤ y.toNNReal ↔ x ≤ y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y

Tactic:
;

Goal state after:
x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ √1 < √2

Tactic:
;

Goal state after:
⊢ √1 < √2
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case h
⊢ 1 < 2

Tactic:
;

Goal state after:
case h
⊢ 1 < 2
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
;

Goal state after:
r : ℝ
⊢ ↑‖↑r‖₊ = ↑‖r‖₊
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q

Tactic:
;

Goal state after:
q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case inr
α : 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
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

Tactic:
apply le_of_eq _
    dsimp
    rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]

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

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

Tactic:
;

Goal state after:
x y : ℝ
⊢ ‖↑x + ↑y * I‖ = √(normSq (↑x + ↑y * I))
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
by simp [hz, zero_le_one]

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

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

Tactic:
by simp [hz, zero_le_one]

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:
rw [lintegral_const_mul']
          finiteness

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.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
⊢ ‖↑f j - ↑f i‖ < ε

Tactic:
;

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖↑f j - ↑f i‖ < ε
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ CauSeq.lim ⟨fun n ↦ -(↑f n).im, ⋯⟩ = (-⟨fun n ↦ (↑f n).im, ⋯⟩).lim

Tactic:
;

Goal state after:
f : CauSeq ℂ fun x ↦ ‖x‖
⊢ CauSeq.lim ⟨fun n ↦ -(↑f n).im, ⋯⟩ = (-⟨fun n ↦ (↑f n).im, ⋯⟩).lim
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ 0 + a✝ = a✝

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ 0 + a✝ = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ + 0 = a✝

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ a✝ + 0 = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x✝ : ℂ
⊢ 0 • x✝ = 0

Tactic:
;

Goal state after:
x✝ : ℂ
⊢ 0 • x✝ = 0
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
n✝ : ℕ
x✝ : ℂ
⊢ (n✝ + 1) • x✝ = n✝ • x✝ + x✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ 0 • a✝ = 0

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ 0 • a✝ = 0
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
n✝ : ℕ
a✝ : ℂ
⊢ ↑n✝.succ • a✝ = ↑n✝ • a✝ + a✝
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
n✝ : ℕ
a✝ : ℂ
⊢ Int.negSucc n✝ • a✝ = -(↑n✝.succ • a✝)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ -a✝ + a✝ = 0

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ -a✝ + a✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
;

Goal state after:
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + 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.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

Tactic:
;

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
Module: Mathlib.Analysis.Complex.Order

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

Tactic:
by rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]

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

Goal state before:
pp: a✝ : ℂ
⊢ 1 * a✝ = a✝

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ 1 * a✝ = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ * 1 = a✝

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ a✝ * 1 = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ 0 * a✝ = 0

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ 0 * a✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ * 0 = 0

Tactic:
;

Goal state after:
a✝ : ℂ
⊢ a✝ * 0 = 0
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝

Tactic:
;

Goal state after:
a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
r : ℝ
⊢ ↑(↑r).re = ↑r
Module: Mathlib.Data.Complex.Basic

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

Tactic:
;

Goal state after:
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re + z.im * w.im)
Module: Mathlib.Data.Complex.Basic

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

Tactic:
rw [inv_eq_one_div, div_I, one_mul]

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

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0
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:
;

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

Goal state after:
ι : 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
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set β
hs : ν s✝ = 0
⊢ (Measure.map (fun z ↦ z.2) (μ.prod ν)) s✝ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : MeasurableSet s✝
⊢ MeasurableSet s✝
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0

Tactic:
;

Goal state after:
case funProp.discharger
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s✝ : Set α
hs : μ s✝ = 0
⊢ (Measure.map (fun z ↦ z.1) (μ.prod ν)) s✝ = 0
Module: Mathlib.Algebra.Order.BigOperators.Expect

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

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
⊢ 0 < (↑(#s))⁻¹
Module: Mathlib.Algebra.Order.BigOperators.Expect

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

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
this : s.Nonempty
⊢ 0 < (↑(#s))⁻¹
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : ∀ x ∈ s, f x ≤ g x
⊢ 𝔼 i ∈ s, f i ≤ 𝔼 i ∈ s, g i

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f g : ι → α
h : ∀ x ∈ s, f x ≤ g x
⊢ 𝔼 i ∈ s, f i ≤ 𝔼 i ∈ s, g i
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ a ≤ 𝔼 i ∈ s, f i
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)

Tactic:
;

Goal state after:
case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
g : A →⋆* B
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
g : A →⋆* B
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } = g
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
toMonoidHom✝¹ : A →* B
map_star'✝¹ : ∀ (a : A), (↑toMonoidHom✝¹).toFun (star a) = star ((↑toMonoidHom✝¹).toFun a)
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } = { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
toMonoidHom✝¹ : A →* B
map_star'✝¹ : ∀ (a : A), (↑toMonoidHom✝¹).toFun (star a) = star ((↑toMonoidHom✝¹).toFun a)
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } = { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }