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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [lintegral_map' hi.aemeasurable hg]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : α), i (g a) ∂μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case refine_1.h₂
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 := ⋯
fs : ∀ x ∈ s, f x = x
⊢ s ⊆ range f

Tactic:
intro x hx
      rw [← fs x hx]
      exact mem_range_self _

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

Goal state before:
pp: case refine_2.inr.inl
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
h' : f x = f y
⊢ dist (f x) (f y) ≤ dist x y

pp: case refine_2.inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
· simp [h']

Goal state after:
case refine_2.inr.inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
⊢ dist (f x) (f y) ≤ dist x y
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

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

Tactic:
← Measure.MutuallySingular.self_iff

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ ⟂ₘ μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ (Measure.comap f μ) univ = 1

Tactic:
rw [comap_apply _ hf hf'' _ MeasurableSet.univ,
      ← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ f '' univ ∈ ae μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = μ (measurableAtom ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩) * 1 ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩

Tactic:
simp only [Pi.one_apply, mul_one]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = μ (measurableAtom (points ⟨measurableAtom x, ⋯⟩))
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_have 3 → 2
  | h => disjoint_of_disjoint_ae h

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
tfae_3_to_2 : Disjoint (ae μ) (ae ν) → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
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
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
have hn : firstDiff x.1 y.1 = n + 1 := (Nat.succ_pred_eq_of_pos diff_pos).symm

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' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
⊢ dist (g x) (g y) ≤ 4 * dist x y
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
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
⊢ dist (g x) (g y) ≤ 4 * dist x y

Tactic:
rw [dist', dist_eq_of_ne hne', hn]

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' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
⊢ dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case succ
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
I : (↑(F (p n))).2.1 m = (↑(p n)).2.1 m
⊢ (↑(p (n + 1))).2.1 m = (↑(p (m + 1))).2.1 m

Tactic:
prec,

Goal state after:
case succ
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
I : (↑(F (p n))).2.1 m = (↑(p n)).2.1 m
⊢ (↑(F (p n))).2.1 m = (↑(p (m + 1))).2.1 m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
i : ι
h : edist x y < 2⁻¹ ^ encode i
⊢ edist (x i) (y i) ≤ edist x y

Tactic:
simpa only [not_le.2 h, false_or] using min_le_iff.1 (min_edist_le_edist_pi x y i)

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

Goal state before:
pp: case succ
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
I : (↑(F (p n))).2.2 m = (↑(p n)).2.2 m
⊢ (↑(p (n + 1))).2.2 m = (↑(p (m + 1))).2.2 m

Tactic:
prec,

Goal state after:
case succ
α : 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
I : (↑(F (p n))).2.2 m = (↑(p n)).2.2 m
⊢ (↑(F (p n))).2.2 m = (↑(p (m + 1))).2.2 m
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 < ↑c * μ t

Tactic:
mul_comm,

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
⊢ ∃ R,
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Ioc 0 K → r ≤ R → μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
refine ⟨R, Rpos, fun x t r ht hr => ?_⟩

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ ↑(Classical.choose ⋯) * μ (closedBall x r) ≤ ↑(max (Classical.choose ⋯) 1) * μ (closedBall x r)

Tactic:
← le_max_left

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr : ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * r)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
x : α
⊢ ↑(Classical.choose ⋯) * μ (closedBall x r) ≤ ↑(Classical.choose ⋯) * μ (closedBall x r)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (if x ∈ toMeasurable μ s then T else ∅) ∂μ = μ (toMeasurable μ s) * ν T

Tactic:
measure_if,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), (toMeasurable μ s).indicator (fun x ↦ ν T) x ∂μ = μ (toMeasurable μ 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 (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x ↦ ν (Prod.mk x ⁻¹' t)) =ᵐ[μ] 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) ≤ᵐ[μ] 0 ∧ 0 ≤ᵐ[μ] fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
exact
    ⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht,
      Eventually.of_forall fun x => zero_le⟩

Goal state after:
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 β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᵐ[ν] Prod.mk x ⁻¹' u
⊢ t =ᵐ[ν] Prod.mk x ⁻¹' u

Tactic:
rwa [mk_preimage_prod_right hxs] at hx

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
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''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
rw [← cmem.card_mul_card]
    refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c • μ U
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K

Tactic:
H.measure_eq_iSup hU,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c • ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
⊢ IsComplement (f • ↑T) ↑H

Tactic:
refine isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_
      obtain ⟨t, ht1, ht2⟩ := isComplement_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)
      refine ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩
      · exact smul_inv_smul f g ▸ QuotientAction.inv_mul_mem f ht1
      · rintro ⟨-, t', ht', rfl⟩ h
        replace h := QuotientAction.inv_mul_mem f⁻¹ h
        simp only [Subtype.ext_iff, smul_left_cancel_iff, inv_smul_smul] at h ⊢
        exact Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq μ i) (if y ∈ t then s else ∅) = (sfiniteSeq μ i) s * (dirac y) t

Tactic:
measure_if,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ t.indicator (fun x ↦ (sfiniteSeq μ i) s) y = (sfiniteSeq μ i) s * (dirac y) t
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq ν i) (if x ∈ s then t else ∅) = (dirac x) s * (sfiniteSeq ν i) t

Tactic:
measure_if,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ s.indicator (fun x ↦ (sfiniteSeq ν i) t) x = (dirac x) s * (sfiniteSeq ν i) t
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
⊢ IsClopenable s ↔ MeasurableSet s

Tactic:
by
  -- we already know that a measurable set is clopenable. Conversely, assume that `s` is clopenable.
  refine ⟨fun hs => ?_, fun hs => hs.isClopenable⟩
  borelize γ
  -- consider a finer topology `t'` in which `s` is open and closed.
  obtain ⟨t', t't, t'_polish, _, s_open⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs
  rw [← borel_eq_borel_of_le t'_polish _ t't]
  · exact MeasurableSpace.measurableSet_generateFrom s_open
  infer_instance

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 γ
δ : 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
⊢ MeasurePreserving (fun p ↦ (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Tactic:
have : Measurable fun p : α × γ => (f p.1, g p.1 p.2) := (hf.1.comp measurable_fst).prodMk hgm
  use this
  /- if `μa = 0`, then the lemma is trivial, otherwise we can use `hg`
    to deduce `SFinite μd`. -/
  rcases eq_zero_or_neZero μa with rfl | _
  · simp [← hf.map_eq]
  have sf : SFinite μd := by
    obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
    rw [← ha]
    infer_instance
  -- Thus we can use the integral formula for the product measure, and compute things explicitly
  ext s hs
  rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs,
    ← hf.lintegral_comp (measurable_measure_prodMk_left hs)]
  apply lintegral_congr_ae
  filter_upwards [hg] with a ha
  rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]

Goal state after:
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✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ x * g) (c • μ) = c • μ

Tactic:
rw [Measure.map_smul, map_mul_right_eq_self]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε

Tactic:
rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : μ A < μ K + ε
⊢ ∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ x * g) μ = μ

Tactic:
mul_comm,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ g * x) μ = μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
by
  rw [ae_iff, ae_iff, withDensity_apply_eq_zero' hf, iff_iff_eq]
  congr
  ext x
  simp only [exists_prop, mem_inter_iff, mem_ofPred_eq, not_forall]

Goal state after: