mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hg : dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
hn : n ≥ N
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢

Goal state after:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
hn : n ≥ N
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
⊢ StronglyMeasurable (uncurry u)

Tactic:
borelize β
  obtain ⟨t_sf, ht_sf⟩ :
    ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) := by
    have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
    refine ⟨h_str_meas.approx, fun j x => ?_⟩
    exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
  let U (n : ℕ) (p : ι × α) := u (t_sf n p.fst) p.snd
  have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) := by
    rw [tendsto_pi_nhds]
    exact fun p => ht_sf p.fst p.snd
  refine stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto
  have h_str_meas : StronglyMeasurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
    refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
    · have :
        (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
          (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
        rfl
      rw [this, measurable_swap_iff]
      exact measurable_from_prod_countable_left fun j => (h j).measurable
    · have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) :=
        .iUnion fun i => (h i).isSeparable_range
      apply this.mono
      rintro _ ⟨⟨i, x⟩, rfl⟩
      simp only [mem_iUnion, mem_range]
      exact ⟨i, x, rfl⟩
  have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl
  simp_rw [U, this]
  refine h_str_meas.comp_measurable (Measurable.prodMk ?_ measurable_snd)
  exact ((t_sf n).measurable.comp measurable_fst).subtype_mk

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n : ℕ
⊢ ∀ (m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
m

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m : ℕ
⊢ ∀ N ≤ n, N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ ↑(σ 0) = ↑1

Tactic:
simp [symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ ↑(σ 1) = ↑0

Tactic:
simp [symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ ↑(σ (σ x)) = ↑x

Tactic:
simp [symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inr.inl
x : { x // x ∈ I }
h₀ : 0 ≤ ↑x
h₁ : ↑x ≤ 1
⊢ ↑(σ (projIcc 0 1 ⋯ ↑x)) = ↑(projIcc 0 1 ⋯ (1 - ↑x))

Tactic:
← coe_symm_eq,

Goal state after:
case inr.inl
x : { x // x ∈ I }
h₀ : 0 ≤ ↑x
h₁ : ↑x ≤ 1
⊢ ↑(σ (projIcc 0 1 ⋯ ↑x)) = ↑(projIcc 0 1 ⋯ ↑(σ x))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : 0 ≤ c - d
⊢ a - a ≤ c - d

Tactic:
by rwa [sub_self]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyMetrizableSpace X
⊢ IsCompletelyPseudoMetrizableSpace X

Tactic:
obtain ⟨m, _⟩ := ‹_›
  use m.toPseudoMetricSpace

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

Goal state before:
pp: case mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) → ∀ i < n, y i = x i

Tactic:
rintro ⟨k, hk⟩ i hi
    simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : u.toTopologicalSpace = ⨅ i, t i
⊢ PolishSpace α

Tactic:
rw [← htop]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : u.toTopologicalSpace = ⨅ i, t i
⊢ PolishSpace α
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) → n ≤ firstDiff y x

pp: case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ i < n, y i = x i

Tactic:
· intro hy
    by_contra! H
    exact apply_firstDiff_ne hne (hy _ H)

Goal state after:
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ i < n, y i = x i
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n ↦ A (res x n)
n : ℕ
⊢ ∀ (m : ℕ), n ≤ m → u m ∈ A (res x n)

Tactic:
m

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n ↦ A (res x n)
n m : ℕ
⊢ n ≤ m → u m ∈ A (res x n)
Module: Mathlib.Topology.MetricSpace.Gluing

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

Tactic:
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]

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

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

Tactic:
measure_empty

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ y ∈ range F

Tactic:
refine ⟨⟨x, xt⟩, ?_⟩

Goal state after:
case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
xt : x ∈ t
⊢ F ⟨x, xt⟩ = y
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite

pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
· exact count_apply_eq_top' hs.measurableSet

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite
Module: Mathlib.MeasureTheory.Measure.Dirac

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

Tactic:
intro h A A_mble

Goal state after:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Measure.Dirac

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

Tactic:
intro h A A_mble
    have obs := congr_arg (fun μ ↦ μ A) h
    simp only [Measure.dirac_apply' _ A_mble] at obs
    by_cases x_in_A : x ∈ A
    · simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)),
                  indicator_eq_one_iff_mem] using obs
    · simpa only [x_in_A, indicator_of_notMem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero,
                  false_iff, not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs

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

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
n : ι
⊢ ∀ (i : ι), Disjoint (t n) (⋂ n, u i n)

Tactic:
m

Goal state after:
case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
n m : ι
⊢ Disjoint (t n) (⋂ n, u m n)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in {a}, f a ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}

Tactic:
lintegral_singleton,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ + f a * μ {a} = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : PiNatEmbed X (fun x ↦ ↑I) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 x.ofPiNat
i : ℕ
t : Set ↑I
ht : t ∈ 𝓝 (distDenseSeq X i x.ofPiNat)
hts : distDenseSeq X i ⁻¹' t ⊆ s
⊢ s ∈ map ofPiNat (comap (embed X (fun i ↦ ↑I) (distDenseSeq X)) (𝓝 (embed X (fun i ↦ ↑I) (distDenseSeq X) x)))

Tactic:
nhds_pi

Goal state after:
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : PiNatEmbed X (fun x ↦ ↑I) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 x.ofPiNat
i : ℕ
t : Set ↑I
ht : t ∈ 𝓝 (distDenseSeq X i x.ofPiNat)
hts : distDenseSeq X i ⁻¹' t ⊆ s
⊢ s ∈
    map ofPiNat
      (comap (embed X (fun i ↦ ↑I) (distDenseSeq X)) (Filter.pi fun i ↦ 𝓝 (embed X (fun i ↦ ↑I) (distDenseSeq X) x i)))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
obtain ⟨s, hs, t, -, rfl⟩ := hs

Goal state after:
case basic
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ : Set (α × β)
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) s t)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (s ×ˢ t)ᶜ = 0

Tactic:
by
  rw [Set.compl_prod_eq_union, measure_union_null_iff]
  simp [s_ae_univ, t_ae_univ]

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
⊢ MeasurableSet (range f)

Tactic:
obtain ⟨b, b_count, b_nonempty, hb⟩ :
    ∃ b : Set (Set γ), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b := exists_countable_basis γ

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
⊢ MeasurableSet (range f)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
· rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩
    exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

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

Goal state before:
pp: case refine_1
α : 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)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ U

pp: case refine_2
α : 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)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ r < (comap f μ) (f ⁻¹' K)

Tactic:
· rw [← hf.injective.preimage_image U]; exact preimage_mono hKU

Goal state after:
case refine_2
α : 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)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ r < (comap f μ) (f ⁻¹' K)
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
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
U : ℕ → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst✝¹] (U n)
hU : ∀ (n : ℕ), μ (U n) < μ (A n) + δ n
⊢ ∃ U ⊇ ⋃ n, A n, IsOpen[inst✝¹] U ∧ μ U < r

Tactic:
refine ⟨⋃ n, U n, iUnion_mono hAU, isOpen_iUnion hUo, ?_⟩

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
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : μ (⋃ n, A n) + ∑' (i : ℕ), δ i < r
U : ℕ → Set α
hAU : ∀ (n : ℕ), U n ⊇ A n
hUo : ∀ (n : ℕ), IsOpen[inst✝¹] (U n)
hU : ∀ (n : ℕ), μ (U n) < μ (A n) + δ n
⊢ μ (⋃ n, U n) < r
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 μ
hBU : ⋃ n, s ∩ B n = s
⊢ μ s = ⨆ n, μ (s ∩ B n)

Tactic:
← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion,

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
⊢ μ s = μ (⋃ i, s ∩ spanningSets μ i)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝²] U
H : μ U ≤ μ s + (r' - μ s)
⊢ μ U < r

Tactic:
rw [add_tsub_cancel_of_le hsr'.le] at H

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝²] U
H : μ U ≤ r'
⊢ μ U < r
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
hs : IsClopenable s
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
⊢ MeasurableSet s

Tactic:
obtain ⟨t', t't, t'_polish, _, s_open⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs

Goal state after:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
⊢ SFinite μd

Tactic:
obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
a : α
ha : map (g a) μc = μd
⊢ SFinite μd
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : MeasurableSpace H✝
inst✝⁷ : Mul G
μ : Measure G
inst✝⁶ : MeasurableMul G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
H : Type u_3
inst✝³ : Mul H
mH : MeasurableSpace H
ν : Measure H
inst✝² : MeasurableMul H
inst✝¹ : ν.IsMulLeftInvariant
inst✝ : SFinite ν
g : G
h : H
⊢ map (Prod.map (fun x ↦ g * x) fun x ↦ h * x) (μ.prod ν) = μ.prod ν

Tactic:
← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),

Goal state after:
G : Type u_1
H✝ : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : MeasurableSpace H✝
inst✝⁷ : Mul G
μ : Measure G
inst✝⁶ : MeasurableMul G
inst✝⁵ : μ.IsMulLeftInvariant
inst✝⁴ : SFinite μ
H : Type u_3
inst✝³ : Mul H
mH : MeasurableSpace H
ν : Measure H
inst✝² : MeasurableMul H
inst✝¹ : ν.IsMulLeftInvariant
inst✝ : SFinite ν
g : G
h : H
⊢ (map (fun x ↦ g * x) μ).prod (map (fun x ↦ h * x) ν) = μ.prod ν