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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n : ℕ
⊢ cylinder y n = cylinder (↑(p n)).2.2 (↑(p n)).1

Tactic:
·

Goal state after:
case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n : ℕ
⊢ cylinder y n = cylinder (↑(p n)).2.2 (↑(p n)).1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case neg.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ < ∞

pp: case neg.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ

Tactic:
·

Goal state after:
case neg.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

pp: case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)

pp: case inr.inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)

pp: case inr.inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rpos : 0 < r
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case neg.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ

Tactic:
·

Goal state after:
case neg.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map ((fun x ↦ x.1 * x.2) ∘ Prod.swap) (ν.prod μ) = map (fun x ↦ x.1 * x.2) (ν.prod μ)

pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable Prod.swap

Tactic:
·

Goal state after:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map ((fun x ↦ x.1 * x.2) ∘ Prod.swap) (ν.prod μ) = map (fun x ↦ x.1 * x.2) (ν.prod μ)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (SimpleFunc.map ofNNReal g₀) a ∂μ

Tactic:
SimpleFunc.coe_map

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
g₀ : α →ₛ ℝ≥0
hg₀ : ∀ (x : α), ↑(g₀ x) ≤ ↑(f x)
g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ
⊢ ∫⁻ (x : α), ↑(g₀ x) ∂μ = ∫⁻ (a : α), (ofNNReal ∘ ⇑g₀) a ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.Dynamics.Minimal

Goal state before:
pp: case mp
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ

pp: case mpr
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
⊢ (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α

Tactic:
·

Goal state after:
case mp
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < μ u

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v

Tactic:
·

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < μ u
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v

Tactic:
·

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ

pp: case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x

Tactic:
·

Goal state after:
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ map (fun x ↦ DomMulAct.mk.symm (g * g')⁻¹ • x) μ =
    map ((fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ∘ fun x ↦ DomMulAct.mk.symm g'⁻¹ • x) μ