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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
rw [hνs, mul_zero]

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  have hF'_le : F' ≤ᵐ[μ] F := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto

Goal state after:
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 ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
⊢ ∃ t, ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t n) j) x) atTop (𝓝 (u j x))

Tactic:
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)

Goal state after:
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)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ t, ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t n) j) x) atTop (𝓝 (u j x))

Tactic:
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)

Goal state after:
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)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
⊢ StronglyMeasurable (uncurry u)

Tactic:
refine stronglyMeasurable_of_tendsto _ (fun n => ?_) h_tendsto

Goal state after:
α : 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)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
⊢ StronglyMeasurable (U n)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ i ≤ σ j ↔ j ≤ σ i

Tactic:
rw [← symm_le_symm, symm_symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ i ≤ j ↔ σ j ≤ i

Tactic:
rw [← symm_le_symm, symm_symm]

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

Goal state before:
pp: X : Type u_3
ht : TopologicalSpace X
h : IsCompletelyPseudoMetrizableSpace X
⊢ completelyPseudoMetrizableMetric X = ⋯.choose

Tactic:
exact PseudoMetricSpace.replaceTopology_eq _ _

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[coinduced (⇑f) instTopologicalSpaceSum] s

Tactic:
· rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]

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

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
⊢ longestPrefix y s = longestPrefix x s

Tactic:
have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
        inter_cylinder_longestPrefix_nonempty hs hne x

Goal state after:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ longestPrefix y s = longestPrefix x s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix x s < longestPrefix y s
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty
Z : Disjoint s (cylinder x (longestPrefix x s).succ)
⊢ longestPrefix y s = longestPrefix x s

Tactic:
cylinder_eq_cylinder_of_le_firstDiff _ _ H

Goal state after:
case inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix x s < longestPrefix y s
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
A'y : (s ∩ cylinder y (longestPrefix x s).succ).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s).succ)
⊢ longestPrefix y s = longestPrefix x s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : 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) μ
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs

Goal state after:
α : 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
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
| (1 / 2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))

Tactic:
enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (fun x ↦ μ {x}) x = μ s

Tactic:
calc
    (∑' x : α, s.indicator (fun x => μ {x}) x) =
      Measure.sum (fun a => μ {a} • Measure.dirac a) s := by
      simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply,
        Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero]
    _ = μ s := by rw [μ.sum_smul_dirac]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ count (f '' s) = count s

Tactic:
lift s to Finset β using hs
    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]
    simpa only [Finset.coe_image] using fs_mble

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

Goal state before:
pp: case refine_1
ι : 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, s n ⊆ ⋃ m, ⋂ n, u m n

Tactic:
refine iUnion_subset fun m => subset_iUnion_of_subset m ?_
    exact subset_iInter fun n => hsu m n

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
⊢ False

Tactic:
have Ix : ∀ m n, m + 1 ≤ n → (p n).1.2.1 m = (p (m + 1)).1.2.1 m := by
    intro m
    apply Nat.le_induction
    · rfl
    intro n hmn IH
    have I : (F (p n)).val.snd.fst m = (p n).val.snd.fst m := by
      apply hFx (p n) m
      rw [pn_fst]
      exact hmn
    rw [prec, I, IH]

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), ⋯⟩
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
⊢ False
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
⊢ 0 < ε → {a | edist (a.1 i) (a.2 i) < ε} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
hε₀

Goal state after:
case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
⊢ {a | edist (a.1 i) (a.2 i) < ε} ∈ ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | edist p.1 p.2 < ε}
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
ε : ℝ
⊢ ε ∈ Ioi 0 →
    (∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)) →
      ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Tactic:
hε₀

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ε₀ : ε ∈ Ioi 0
⊢ (∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)) →
    ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑C * μ (closedBall x ε)

Tactic:
by
  let C := doublingConstant μ
  suffices ∀ n,
      ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x ((2 : ℝ) ^ n * ε)) ≤ C ^ n * μ (closedBall x ε) by
    rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩
    use C ^ n
    filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht
    rw [mem_Ioi] at hε₀
    grw [ht, hn, ENNReal.coe_pow]
    exact hε x
  intro n
  induction n with
  | zero => simp
  | succ n ihn =>
    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.Integral.Lebesgue.Countable

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

Tactic:
refine ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩

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

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : 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
this : SigmaFinite ν
⊢ univ ×ˢ ⋃ n, hν.set n = univ

Tactic:
hν.spanning,

Goal state after:
case refine_2
α : 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
this : SigmaFinite ν
⊢ univ ×ˢ univ = univ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
⊢ μ (univ ×ˢ univ) = ν (univ ×ˢ univ)

Tactic:
exact h .univ .univ

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g

Tactic:
equiv,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (Equiv.ofBijective (fun x ↦ ↑x.1 * ↑x.2) hST).symm.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g

Tactic:
equiv,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (Equiv.ofBijective (fun x ↦ ↑x.1 * ↑x.2) hST).symm.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = f q

Tactic:
by
  refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
  exact (leftQuotientEquiv (isComplement_range_left hf)).eq_symm_apply.mp (hf q).symm

Goal state after:
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s ∩ (c * c⁻¹) • t) = μ (c • s ∩ t)

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s ∩ 1 • t) = μ (c • s ∩ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s ∪ (c * c⁻¹) • t) = μ (c • s ∪ t)

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s ∪ 1 • t) = μ (c • s ∪ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s \ (c * c⁻¹) • t) = μ (c • s \ t)

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (c • s \ 1 • t) = μ (c • s \ t)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ ((c • s) ∆ ((c * c⁻¹) • t)) = μ ((c • s) ∆ t)

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ ((c • s) ∆ (1 • t)) = μ ((c • s) ∆ t)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ StandardBorelSpace ↑s

Tactic:
obtain ⟨_, _, _, s_closed, _⟩ := hs.isClopenable'
  have := s_closed.polishSpace
  infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Group.LIntegral

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]

Goal state after: