mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let g' : ℕ → α → ℝ≥0∞ := Nat.rec (g 0) (fun n I x ↦ max (g (n + 1) x) (I x))

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
⊢ Summable f ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
summable_iff_cauchySeq_finset,

Goal state after:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
⊢ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : (U ∩ C).Countable
this : U ∈ v
⊢ x ∈ V

Tactic:
exact mem_biUnion this xU

Goal state after:
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z

Tactic:
· linarith [dist_triangle_left z (Ψ p) y]

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ TopologicalSpace.IsCompletelyMetrizableSpace X

Tactic:
by
  let := upgradeIsCompletelyMetrizable Y
  let : MetricSpace X := hf.isEmbedding.comapMetricSpace f
  have : CompleteSpace X := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
  infer_instance

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
by_cases x = y

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝ : ¬x = y
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
⊢ {a | a.1 n = a.2 n} ∈ ⨅ (_ : (1 / 2) ^ n > 0), 𝓟 {p | dist p.1 p.2 < (1 / 2) ^ n}

Tactic:
refine mem_iInf_of_mem (by positivity) ?_

Goal state after:
case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
n : ℕ
⊢ {a | a.1 n = a.2 n} ∈ 𝓟 {p | dist p.1 p.2 < (1 / 2) ^ n}
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (f m (leRecOn xm (fun {k} ↦ f k) x.snd)) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
leRecOn_succ ym,

Goal state after:
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ m.succ
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (f m (leRecOn xm (fun {k} ↦ f k) x.snd)) (f m (leRecOn ym (fun {k} ↦ f k) y.snd))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < Nat.find A

Tactic:
have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s
this✝ : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
this : ∀ i < n, ∀ j < n, i ≠ j → f^[i] x ∈ s → f^[j] x ∈ s → i < j → ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
hlt : ¬i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
exact this j hj i hi hij.symm hxj hxi (hij.lt_or_gt.resolve_left hlt)

Goal state after:
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 : x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∈ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff x (f y)

Tactic:
rw [fs y ys]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
⊢ False

Tactic:
have : μ Set.univ = 0 := by
    rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
this : μ univ = 0
⊢ False
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ μ1.real {x} = μ2.real {x}

Tactic:
rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : Countable α
μ1 μ2 : Measure α
inst✝¹ : SigmaFinite μ1
inst✝ : SigmaFinite μ2
x : α
⊢ μ1 {x} = μ2 {x} ↔ μ1 {x} = μ2 {x} ∨ μ1 {x} = 0 ∧ μ2 {x} = ∞ ∨ μ1 {x} = ∞ ∧ μ2 {x} = 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

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

Tactic:
union_eq_compl_compl_inter_compl,

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

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

Tactic:
union_eq_compl_compl_inter_compl,

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

Goal state before:
pp: α : 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)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)

Tactic:
← iUnion_cylinder_update x n,

Goal state after:
α : 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)
n : ℕ
x y : ℕ → ℕ
H :
  ∀ (x' y' : ℕ → ℕ),
    x' ∈ cylinder x n → y' ∈ cylinder y n → MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
⊢ MeasurablySeparable (f '' ⋃ k, cylinder (update x n k) (n + 1)) (g '' cylinder y n)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : 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
⊢ ¬MeasurablySeparable (f '' cylinder (0, fun x ↦ 0, fun x ↦ 0).2.1 (0, fun x ↦ 0, fun x ↦ 0).1)
      (g '' cylinder (0, fun x ↦ 0, fun x ↦ 0).2.2 (0, fun x ↦ 0, fun x ↦ 0).1)

Tactic:
by simp [hfg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
⊢ ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m

Tactic:
measure_iUnion h hf

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
⊢ ∫⁻ (μ : Measure α), ∑' (i : ℕ), μ (f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)
⊢ f univ ≤ C

Tactic:
let S := @spanningSets _ m (μ.trim hm) _

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)
S : ℕ → Set α := spanningSets (μ.trim hm)
⊢ f univ ≤ C
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : 0 < ε
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (2 ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Tactic:
ENNReal.coe_pow

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : 0 < ε
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
t : ℝ
ht : t ≤ K
⊢ μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
⊢ dirac 1 ∗ₘ μ = μ

Tactic:
by
  simp [dirac_mconv]

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 ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ (μ.prod ν) (univ ×ˢ univ) = 1

Tactic:
prod_prod,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ μ univ * ν univ = 1
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 ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ (μ.prod ν) (Metric.closedBall x.1 (2 * r) ×ˢ Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x r)

Tactic:
prod_prod,

Goal state after:
α : 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✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ μ (Metric.closedBall x.1 (2 * r)) * ν (Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x r)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' (S * ↑H'') = ↑H

Tactic:
cmem.mul_eq

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' univ = ↑H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : ⇑H.subtype '' (↑H'' * S) = ↑(map H.subtype H'') * ⇑H.subtype '' S
⊢ ⇑H.subtype '' (↑H'' * S) = ↑H

Tactic:
cmem.mul_eq

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : ⇑H.subtype '' (↑H'' * S) = ↑(map H.subtype H'') * ⇑H.subtype '' S
⊢ ⇑H.subtype '' univ = ↑H
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 μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) (t ×ˢ s) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
prod_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq μ i.2) t * (sfiniteSeq ν i.1) s = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t
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 ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
⊢ map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)

Tactic:
have : sum (fun (p : ℕ × ℕ × ℕ) ↦
        (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
      = sum (fun (p : (ℕ × ℕ) × ℕ) ↦
        (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
    simp only [Equiv.prodAssoc_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
this :
  (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
    sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
⊢ map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
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 ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
this :
  (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
    sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
u : Set γ
hu : MeasurableSet u
⊢ (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) ((s ×ˢ t) ×ˢ u) =
    (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) (t ×ˢ u)

Tactic:
prod_prod,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
this :
  (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
    sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
u : Set γ
hu : MeasurableSet u
⊢ (sfiniteSeq μ i.1.1) s * (sfiniteSeq ν i.1.2) t * (sfiniteSeq τ i.2) u =
    (sfiniteSeq μ i.1.1) s * ((sfiniteSeq ν i.1.2) t * (sfiniteSeq τ i.2) u)
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 β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) ((s' ∩ s) ×ˢ (t' ∩ t)) =
    ((sfiniteSeq μ i.1).restrict s) s' * ((sfiniteSeq ν i.2).restrict t) t'

Tactic:
prod_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ (sfiniteSeq μ i.1) (s' ∩ s) * (sfiniteSeq ν i.2) (t' ∩ t) =
    ((sfiniteSeq μ i.1).restrict s) s' * ((sfiniteSeq ν i.2).restrict t) t'
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 μ
ν' : Measure β
inst✝ : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) (s ×ˢ t) + ((sfiniteSeq μ i.1).prod (sfiniteSeq ν' i.2)) (s ×ˢ t) =
    (sfiniteSeq μ i.1) s * ((sfiniteSeq ν i.2) t + (sfiniteSeq ν' i.2) t)

Tactic:
prod_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (sfiniteSeq μ i.1) s * (sfiniteSeq ν i.2) t + (sfiniteSeq μ i.1) s * (sfiniteSeq ν' i.2) t =
    (sfiniteSeq μ i.1) s * ((sfiniteSeq ν i.2) t + (sfiniteSeq ν' i.2) t)