mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ i,
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ

Tactic:
suffices ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1) = μ.sigmaFiniteSetWRT' ν by
      rw [this, Set.compl_union_self]

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ n,
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
⊢ CauchySeq (f ∘ u)

Tactic:
by
  rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
  refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
  · exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
  · exact fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)
  · rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Ici ↑x = Icc x 1

Tactic:
by
  rw [preimage_subtype_val_Ici]
  exact Icc_top.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
wlog hdc : d ≤ c generalizing c d

Goal state after:
case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c✝ d✝ : α
h : a ≤ b
c d : α
hdc : d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:

Tactic:
x (firstDiff x z) = y (firstDiff x z) := apply_eq_of_lt_firstDiff H.1
    _ = z (firstDiff x z) := apply_eq_of_lt_firstDiff H.2

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

Goal state before:
pp: case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
⊢ z ∈ cylinder x n

Tactic:
i

Goal state after:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
⊢ i < n → z i = x i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
⊢ z ∈ cylinder y n

Tactic:
i

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
⊢ i < n → z i = y i
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
n : ℕ
hn : n ≥ N
⊢ u n = u N

Tactic:
specialize hN n hn

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
N n : ℕ
hN : dist (u n) (u N) < 1
hn : n ≥ N
⊢ u n = u N
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
i

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
    · rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩
      exact ⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩
    · rcases h x hx with ⟨ε, ε0, hε⟩
      simp only [dist_eq, one_div] at hε
      have : Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|)
          (𝓝 x) (𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) := by
        refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs
        refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
        rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
        exact x.2
      simp only [dist_self, sub_self, abs_zero, zero_add] at this
      exact mem_of_superset (this <| gt_mem_nhds ε0) hε

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)

Tactic:
have := x.property.some_mem

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some ⋯ ∈ ⋂ n, A (res (↑x) n)
⊢ (inducedMap A).snd x ∈ A (res (↑x) n)
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
⊢ CompleteSpace s.CompleteCopy

Tactic:
refine Metric.complete_of_convergent_controlled_sequences ((1 / 2) ^ ·) (by simp) fun u hu ↦ ?_
  have A : CauchySeq fun n => (u n).1 := by
    refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
    · exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le
    · exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)
  obtain ⟨x, xlim⟩ : ∃ x, Tendsto (fun n => (u n).1) atTop (𝓝 x) := cauchySeq_tendsto_of_complete A
  by_cases xs : x ∈ s
  · exact ⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩
  obtain ⟨C, hC⟩ : ∃ C, ∀ n, 1 / infDist (u n).1 sᶜ < C := by
    refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
    rw [← sub_lt_iff_lt_add]
    calc
      _ ≤ |1 / infDist (u n).1 sᶜ - 1 / infDist (u 0).1 sᶜ| := le_abs_self _
      _ = |1 / infDist (u 0).1 sᶜ - 1 / infDist (u n).1 sᶜ| := abs_sub_comm _ _
      _ ≤ dist (u 0) (u n) := le_add_of_nonneg_left dist_nonneg
      _ < (1 / 2) ^ 0 := hu 0 0 n le_rfl n.zero_le
  have Cpos : 0 < C := lt_of_le_of_lt (div_nonneg zero_le_one infDist_nonneg) (hC 0)
  have Hmem : ∀ {y}, y ∈ s ↔ 0 < infDist y sᶜ := fun {y} ↦ by
    rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]; exact not_not.symm
  have I : ∀ n, 1 / C ≤ infDist (u n).1 sᶜ := fun n ↦ by
    have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
    rw [div_le_iff₀' Cpos]
    exact (div_le_iff₀ this).1 (hC n).le
  have I' : 1 / C ≤ infDist x sᶜ :=
    have : Tendsto (fun n => infDist (u n).1 sᶜ) atTop (𝓝 (infDist x sᶜ)) :=
      ((continuous_infDist_pt (sᶜ : Set α)).tendsto x).comp xlim
    ge_of_tendsto' this I
  exact absurd (Hmem.2 <| lt_of_lt_of_le (div_pos one_pos Cpos) I') xs

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

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i ↦ Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ univ = ⋃ i, s i

Tactic:
simp only [s, ← preimage_iUnion, iUnion_of_singleton, preimage_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SigmaFinite μb
⊢ SigmaFinite (map f μa)

Tactic:
by rwa [hf.map_eq]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ = 0

Tactic:
rw [← Measure.MutuallySingular.self_iff]
  exact h_ms.mono_ac Measure.AbsolutelyContinuous.rfl h_ac

Goal state after:
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:
← compl_union,

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: case isOpen
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (U : Set α), IsOpen[inst✝³] U → IsClopenable U

pp: case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

pp: case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
· exact fun u hu => hu.isClopenable

Goal state after:
case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:

Tactic:
count
      = count.restrict univ := by simp
    _ = count.restrict {i} := by congr; ext j; simp [Subsingleton.elim j i]
    _ = dirac i := by simp

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
have hne' : x.1 ≠ y.1 := Subtype.coe_injective.ne hne

Goal state after:
case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y
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
⊢ False

Tactic:
let p0 : A := ⟨⟨0, fun _ => 0, fun _ => 0⟩, by simp [hfg]⟩

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)
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), ⋯⟩
⊢ False
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫⁻ (x : α), f x ∂μ = c

Tactic:
by simp [lintegral_congr_ae hf]

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

Goal state before:
pp: 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) ∂μ

Tactic:
simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]

Goal state after:
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 < ↑c * μ t
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
    filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x
    grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]

Goal state after:
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
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
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
u v : Set α
u_open : IsOpen[inst✝³] u
v_open : IsOpen[inst✝³] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ ∃ εx > 0, ball x εx ⊆ f ⁻¹' u

Tactic:
apply Metric.mem_nhds_iff.1

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)
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 := ⋯
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 := ⋯
p : ℕ → A := ⋯
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 : ℕ → ℕ := ⋯
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := ⋯
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
u v : Set α
u_open : IsOpen[inst✝³] u
v_open : IsOpen[inst✝³] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ f ⁻¹' u ∈ 𝓝 x
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
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
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
u v : Set α
u_open : IsOpen[inst✝³] u
v_open : IsOpen[inst✝³] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
εx : ℝ
εxpos : εx > 0
hεx : ball x εx ⊆ f ⁻¹' u
⊢ ∃ εy > 0, ball y εy ⊆ g ⁻¹' v

Tactic:
apply Metric.mem_nhds_iff.1

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)
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 := ⋯
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 := ⋯
p : ℕ → A := ⋯
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 : ℕ → ℕ := ⋯
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := ⋯
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
u v : Set α
u_open : IsOpen[inst✝³] u
v_open : IsOpen[inst✝³] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
εx : ℝ
εxpos : εx > 0
hεx : ball x εx ⊆ f ⁻¹' u
⊢ g ⁻¹' v ∈ 𝓝 y
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ dirac x ∗ₘ μ = map (fun y ↦ x * y) μ

Tactic:
unfold mconv

Goal state after:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
x : M
μ : Measure M
inst✝ : SFinite μ
⊢ map (fun x ↦ x.1 * x.2) ((dirac x).prod μ) = map (fun y ↦ x * y) μ
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 μ
x : M
⊢ μ ∗ₘ dirac x = map (fun y ↦ y * x) μ

Tactic:
unfold mconv

Goal state after:
M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableMul₂ M
μ : Measure M
inst✝ : SFinite μ
x : M
⊢ map (fun x ↦ x.1 * x.2) (μ.prod (dirac x)) = map (fun y ↦ y * x) μ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ 0 ∗ₘ μ = 0

Tactic:
unfold mconv

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x ↦ x.1 * x.2) (Measure.prod 0 μ) = 0
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ μ ∗ₘ 0 = 0

Tactic:
unfold mconv

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : MeasurableSpace M
μ : Measure M
⊢ map (fun x ↦ x.1 * x.2) (μ.prod 0) = 0
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ (s • μ) ∗ₘ ν = s • μ ∗ₘ ν

Tactic:
unfold mconv

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ map (fun x ↦ x.1 * x.2) ((s • μ).prod ν) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)