mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y)
⊢ firstDiff x y ≤ firstDiff (f x) y

Tactic:
rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ ν (s ∪ h.nullSet)ᶜ = 0

Tactic:
compl_union

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ ν (sᶜ ∩ h.nullSetᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
⊢ count s = ∞

Tactic:
refine top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)
  rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
  calc
    (#t : ℝ≥0∞) = ∑ i ∈ t, 1 := by simp
    _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
    _ ≤ count (t : Set α) := le_count_apply
    _ ≤ count s := measure_mono ht

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A

Tactic:
have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true]
      simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A,
                 not_false_eq_true, indicator_of_notMem]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (map f m).join s = ∫⁻ (a : α), (f a) s ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ (m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ (map f m).join s ≤ ∫⁻ (a : α), (f a) s ∂m
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ m i).bind f = sum fun i ↦ (m i).bind f

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (map f (sum fun i ↦ m i)).join = sum fun i ↦ (map f (m i)).join
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • m).bind f = c • m.bind f

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (map f (c • m)).join = c • (map f m).join
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x) s ∂f a ∂m = (m.bind fun a ↦ (f a).bind g) s

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (g a) s) (m.bind f)

Tactic:
bind_apply hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x) s ∂f a ∂m = ∫⁻ (a : α), ((f a).bind g) s ∂m

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (f a).bind g) m

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (g a) s) (m.bind f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩

Goal state after:
case const.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
x : α
⊢ (piecewise t ht (const α c) (const α 0)) x ≤ (piecewise s hs (const α c) (const α 0)) x

case const.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ < ∞

case const.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ L < ∫⁻ (x : α), ↑((piecewise t ht (const α c) (const α 0)) x) ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (m.bind fun x ↦ dirac (f x)) = (map f m).bind dirac

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (map (fun x ↦ dirac (f x)) m).join = (map f m).bind dirac
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (map (fun x ↦ dirac (f x)) m).join = (map f m).bind dirac

Tactic:
bind,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (map (fun x ↦ dirac (f x)) m).join = (map dirac (map f m)).join
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = μ.bind id

Tactic:
bind,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = (map id μ).join
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝ : SFinite ν✝
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
⊢ (μ.prod ν).FiniteSpanningSetsIn (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
haveI := hν.sigmaFinite
  refine
    ⟨fun n => hμ.set n.unpair.1 ×ˢ hν.set n.unpair.2, fun n =>
      mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), fun n => ?_, ?_⟩
  · rw [prod_prod]
    exact mul_lt_top (hμ.finite _) (hν.finite _)
  · simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
⊢ (comap f μ).InnerRegularWRT pa qa

Tactic:
intro U hU r hr
  rw [hf.comap_apply] at hr
  obtain ⟨K, hKU, hK, hμU⟩ := H (hAB U hU) r hr
  have hKrange := hKU.trans (image_subset_range _ _)
  refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩
  · rw [← hf.injective.preimage_image U]; exact preimage_mono hKU
  · rwa [hf.comap_apply, image_preimage_eq_iff.mpr hKrange]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Tactic:
coe_mul,

Goal state after:
case snd
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑(hSK.equiv g).2 * ↑k
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.fst
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).1 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).1

Tactic:
coe_mul,

Goal state after:
case refine_2.fst
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).1 = ↑h * ↑(hHT.equiv g).1
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ A = A ∩ univ

Tactic:
inter_univ

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ A = A
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : ↥H
h' : ↑↑H
h1 : ↑(h * h') = 1
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ ↑(h', ⟨g, hg⟩).2 = ↑(h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩).2

Tactic:
coe_mul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : ↥H
h' : ↑↑H
h1 : ↑h * ↑h' = 1
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ ↑(h', ⟨g, hg⟩).2 = ↑(h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩).2
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < μ F
⊢ F ∩ univ = F

Tactic:
inter_univ

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < μ F
⊢ F = F
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ (f ⁻¹' (fun x ↦ m • x) ⁻¹' S) = μ ((fun x ↦ m • f x) ⁻¹' S)

Tactic:
rw [preimage_preimage]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ s ∩ univ = s

Tactic:
inter_univ

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ s = s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
by
  rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict,
    setLIntegral_prod]
  · rfl
  · refine AEMeasurable.comp_measurable ?_ measurable_swap
    convert! hf
    rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ univ = 1

Tactic:
exact measure_univ

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ μ (X ⁻¹' s ∩ univ) = μ (X ⁻¹' s)

Tactic:
inter_univ

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ μ (X ⁻¹' s) = μ (X ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ Measurable ↿fun a ↦ L.support.mulIndicator (fun i ↦ f i) x✝¹.down

Tactic:
rw [Set.mulIndicator]

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ Measurable ↿fun a ↦ if x✝¹.down ∈ L.support then f x✝¹.down else 1
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

Tactic:
exact aemeasurable_one

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : ¬HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable 1 μ

Tactic:
exact aemeasurable_one

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable 1 μ

Tactic:
exact aemeasurable_one

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ

Tactic:
exact aemeasurable_one

Goal state after:
case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : ¬Multipliable (fun i ↦ f i) L
⊢ AEMeasurable 1 μ

Tactic:
exact aemeasurable_one

Goal state after: