mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (f '' s)

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (range (f ∘ g))
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Tactic:
← sum_cond,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ (sum fun b ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ μ s = 0

Tactic:
rw [this]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : ν₁ s = 0
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : μ t = 0
htν₂ : ν₂ tᶜ = 0
this : μ s = μ (s ∩ tᶜ)
⊢ μ (s ∩ tᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν

Tactic:
rw [mem_ae_iff, compl_union]
    exact measure_inter_null_of_null_right _ h.measure_compl_nullSet

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

Tactic:
have prec : ∀ n, p (n + 1) = F (p n) := fun n => by simp only [p, iterate_succ', Function.comp]

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)
⊢ False
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (dirac b) s

Tactic:
simp_rw [dirac_apply' _ hs]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ s.indicator 1 b
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
    refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
    rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]
    exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)

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

Goal state before:
pp: α : 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
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
n : ℕ
hn : n ≤ N
this : x n = y n
⊢ closedBall (u (x n)) ((1 / 2) ^ n) = closedBall (u (y n)) ((1 / 2) ^ n)

Tactic:
rw [this]

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

Goal state before:
pp: α : 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
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
s_closed : IsClosed s
f : (ℕ → ℕ) → ↑s
f_surj : Surjective f
f_cont : Continuous f
⊢ ∃ f, Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧ Surjective f

Tactic:
exact ⟨g ∘ f, g_cont.comp f_cont, g_surj.comp f_surj⟩

Goal state after:
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
  rw [dirac_prod, map_map (by fun_prop) (by fun_prop)]
  simp [Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
⊢ ∃ C,
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : X × Y), (μ.prod ν) (Metric.closedBall x (2 * ε)) ≤ ↑C * (μ.prod ν) (Metric.closedBall x ε)

Tactic:
use doublingConstant μ * doublingConstant ν

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : X × Y),
      (μ.prod ν) (Metric.closedBall x (2 * ε)) ≤
        ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
this : μ.prod ν = sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (μ.prod ν)

Tactic:
rw [this]

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
this : μ.prod ν = sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))
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 γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
this : range f = ⋂ n, F n
E_meas : ∀ (s : ↑b), MeasurableSet (E s)
F_meas : ∀ (n : ℕ), MeasurableSet (F n)
⊢ MeasurableSet (range f)

Tactic:
rw [this]

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
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
this : range f = ⋂ n, F n
E_meas : ∀ (s : ↑b), MeasurableSet (E s)
F_meas : ∀ (n : ℕ), MeasurableSet (F n)
⊢ MeasurableSet (⋂ n, F n)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Nat.card ↑T = H.index

Tactic:
h.card_right

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ H.index = H.index
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ ∃ K ⊆ U, pb K ∧ r < (map f μ) K

Tactic:
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ r < (map f μ) (f '' K)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
K : Set α
hKU : K ⊆ ⇑f ⁻¹' U
hKc : pa K
hK : r < μ K
⊢ r < (map (⇑f) μ) (⇑f '' K)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: 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, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
rw [this]

Goal state after:
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, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
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 < μ (f '' f ⁻¹' K)

Tactic:
image_preimage_eq_iff.mpr hKrange

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 < μ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: 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, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Tactic:
rw [this]

Goal state after:
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, ↑(map H.subtype H'') * S = ↑H ∧ Nat.card ↥(map H.subtype H'') * Nat.card ↑S = Nat.card ↥H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)

Tactic:
simp [LeftCosetEquivalence, leftCoset_eq_iff]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
⊢ LeftCosetEquivalence (↑K) (g * ↑k) g

Tactic:
simp [LeftCosetEquivalence, leftCoset_eq_iff]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case fst
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

Tactic:
rw [this]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.snd
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Tactic:
rw [this]

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 : Set α
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
⊢ MeasurableSet t'

Tactic:
rw [this]

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
⊢ MeasurableSet (⋃ c ∈ u, t ∩ g ⁻¹' {c})
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t)

Tactic:
rw [this]

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun y ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : τ s = 0
⊢ ∫⁻ (x : α), ν ((fun x_1 ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0

Tactic:
rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]

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✝⁶ : 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 ν
⊢ (μ.prod ν).IsMulLeftInvariant

Tactic:
constructor
  rintro ⟨g, h⟩
  change map (Prod.map (g * ·) (h * ·)) (μ.prod ν) = μ.prod ν
  rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]

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✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x * g) μ.inv = μ.inv

Tactic:
conv_rhs => rw [← map_mul_left_eq_self μ g⁻¹]

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x * g) μ.inv = (map (fun x ↦ g⁻¹ * x) μ).inv
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t)

Tactic:
rw [this]

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
y : G
hy : y ∈ (fun x ↦ g * x) ⁻¹' s
⊢ f y ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s

Tactic:
exact ⟨g * y, hy, by simp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ.fst univ = 1

Tactic:
rw [fst_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ univ = 1