mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝¹⁰ : Zero α
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : OpensMeasurableSpace Y
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetrizableSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] f
h'f : HasCompactSupport f
⊢ Measurable f

Tactic:
let : PseudoMetricSpace α := TopologicalSpace.pseudoMetrizableSpacePseudoMetric α
  obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have : ∀ n, ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < u n :=
    fun n ↦ h'f.exists_simpleFunc_approx_of_prod hf (u_pos n)
  choose g hg using this
  have A : ∀ x, Tendsto (fun n ↦ g n x) atTop (𝓝 (f x)) := by
    intro x
    rw [tendsto_iff_dist_tendsto_zero]
    apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
    rw [dist_comm]
    exact (hg n x).le
  apply measurable_of_tendsto_metrizable (fun n ↦ (g n).measurable) (tendsto_pi_nhds.2 A)

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

Goal state before:
pp: case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
y : α
⊢ ⨅ x, f x ≤ f y

Tactic:
exact iInf_le _ _

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable id (Measure.map f μ)

Tactic:
refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ (Measure.map f μ) (closure[inst✝²] t)ᶜ = 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
⊢ ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r}) =
    ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a})

Tactic:
by
      simp only [(eq _).symm]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
x : α
hx : 0 x ≤ f x
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)

Tactic:
Real.enorm_eq_ofReal hx

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
x : α
hx : 0 x ≤ f x
⊢ ENNReal.ofReal (f x) = ENNReal.ofReal (f x)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure[inst✝³] (⋃ i, range (f (v i))))
x : α
⊢ g x ∈ closure[inst✝³] (⋃ i, range (f (v i)))

Tactic:
tendsto_pi_nhds

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable (closure[inst✝³] (⋃ i, range (f (v i))))
x : α
⊢ g x ∈ closure[inst✝³] (⋃ i, range (f (v i)))
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
⊢ ⋃ i, f (e i) = Set.univ

Tactic:
simp only [Nat.pairEquiv_symm_apply, f, e]
    rw [← Set.union_iUnion]
    suffices ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1) = μ.sigmaFiniteSetWRT' ν by
      rw [this, Set.compl_union_self]
    calc ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1)
      = ⋃ n, ⋃ m, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n) :=
          Set.iUnion_unpair (fun n m ↦ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n)
    _ = ⋃ n, μ.sigmaFiniteSetGE ν n := by
        refine Set.iUnion_congr (fun n ↦ ?_)
        rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
    _ = μ.sigmaFiniteSetWRT' ν := rfl

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
⊢ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ D, y ≠ x

Tactic:
E

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
⊢ E ∈ 𝓝 x → ∃ y ∈ E ∩ D, y ≠ x
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_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
⊢ Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)

Tactic:
tendsto_pi_nhds

Goal state after:
α : 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_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
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False

Tactic:
h,

Goal state after:
case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ ∅
h : D = ∅
⊢ False
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
⊢ Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)

Tactic:
tendsto_pi_nhds

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
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)

Tactic:
simp only [glueDist]

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
⊢ min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z

Tactic:
by
  by_contra! H
  rw [lt_min_iff] at H
  refine apply_firstDiff_ne h ?_
  calc
    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.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
⊢ x m = y m

Tactic:
rcases hm with hm | hm

Goal state after:
case mp.succ.inl
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m < n
⊢ x m = y m

case mp.succ.inr
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
x y z : s.CompleteCopy
⊢ dist x z ≤ dist x y + dist y z

Tactic:
calc
      dist x z = dist x.1 z.1 + |1 / infDist x.1 sᶜ - 1 / infDist z.1 sᶜ| := rfl
      _ ≤ dist x.1 y.1 + dist y.1 z.1 + (|1 / infDist x.1 sᶜ - 1 / infDist y.1 sᶜ| +
            |1 / infDist y.1 sᶜ - 1 / infDist z.1 sᶜ|) :=
        add_le_add (dist_triangle _ _ _) (dist_triangle (1 / infDist _ _) _ _)
      _ = dist x y + dist y z := add_add_add_comm ..

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

Goal state before:
pp: α : Type u_1
t : TopologicalSpace α
inst✝ : PolishSpace α
s : ℕ → Set α
m : ℕ → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h✝ : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
⊢ IsClopenable (⋃ n, s n)

Tactic:
obtain ⟨t', t'm, -, t'_polish⟩ :
      ∃ t' : TopologicalSpace α, (∀ n : ℕ, t' ≤ m n) ∧ t' ≤ t ∧ @PolishSpace α t' :=
    exists_polishSpace_forall_le m mt m_polish

Goal state after:
α : Type u_1
t : TopologicalSpace α
inst✝ : PolishSpace α
s : ℕ → Set α
m : ℕ → TopologicalSpace α
mt : ∀ (n : ℕ), m n ≤ t
m_polish : ∀ (n : ℕ), PolishSpace α
h✝ : ∀ (n : ℕ), IsClosed[m n] (s n)
m_open : ∀ (n : ℕ), IsOpen[m n] (s n)
t' : TopologicalSpace α
t'm : ∀ (n : ℕ), t' ≤ m n
t'_polish : PolishSpace α
⊢ IsClopenable (⋃ n, s n)
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
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
← hf.map_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = (map f μa).restrict s
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
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
← hf.map_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
⊢ map f (μa.restrict (f ⁻¹' s)) = (map f μa).restrict s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb

Tactic:
← hf.map_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g (map f μa)
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
hfe : MeasurableEmbedding f
s : Set β
⊢ μa (f ⁻¹' s) = μb s

Tactic:
← hf.map_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
hfe : MeasurableEmbedding f
s : Set β
⊢ μa (f ⁻¹' s) = (map f μa) s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

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

Tactic:
have A : ∀ n, ∃ x : β n, f n x = y := by
        intro n
        rw [← mem_range, f_range n]
        exact mem_iInter.1 hy n

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ (sum fun b ↦ f b • dirac b) {a} = f a

Tactic:
by
  simp +contextual [tsum_eq_single a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ (map f (dirac a)) s = (dirac (f a)) s

Tactic:
map_apply_of_aemeasurable (by fun_prop) hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ (dirac a) (f ⁻¹' s) = (dirac (f a)) s
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
E : ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) = ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty

Tactic:
E

Goal state after:
α : 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
E : ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) = ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)).Nonempty
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✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
⊢ ∫⁻ (a : M), s.indicator 1 a ∂μ ∗ₘ ν = 0

Tactic:
lintegral_mconv (by measurability)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
⊢ ∫⁻ (x : M), ∫⁻ (y : M), s.indicator 1 (x * y) ∂ν ∂μ = 0
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 ν
⊢ ⋃ i, hμ.set (Nat.unpair i).1 ×ˢ hν.set (Nat.unpair i).2 = univ

Tactic:
iUnion_unpair_prod,

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 ν
⊢ (⋃ n, hμ.set n) ×ˢ ⋃ n, hν.set n = univ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (Subtype.val '' Subtype.val ⁻¹' s) ↔ MeasurableSet (range f ∩ s)

Tactic:
Subtype.image_preimage_coe

Goal state after:
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
f : X → Z
inst✝ : CountablySeparated ↑(range f)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (range f ∩ s) ↔ MeasurableSet (range f ∩ s)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case e'_2
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! s, (↑s)⁻¹ * g ∈ T) ↔ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
constructor <;> rintro ⟨x, hx, hx'⟩

Goal state after:
case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s ↦ (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case e'_2
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! t, g * (↑t)⁻¹ ∈ S) ↔ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
constructor <;> rintro ⟨x, hx, hx'⟩

Goal state after:
case e'_2.mp
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t ↦ g * (↑t)⁻¹ ∈ S) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! t, g * (↑t)⁻¹ ∈ S
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : 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
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ univ - μ t = ν univ - ν t

Tactic:
h,

Goal state after:
case refine_2
α : 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
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ univ - ν t = ν univ - ν t