mathlib-initiative/mathlib-tactics huggingface dataset:
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
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable (U n)

Tactic:
U,

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
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
h_meas : Measurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ Measurable fun p ↦ u ((t_sf n) p.1) p.2
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)
n : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable (U n)

Tactic:
U,

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 : ℕ
h_str_meas : StronglyMeasurable fun p ↦ u (↑p.1) p.2
this : (fun p ↦ u ((t_sf n) p.1) p.2) = (fun p ↦ u (↑p.1) p.2) ∘ fun p ↦ (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable fun p ↦ u ((t_sf n) p.1) p.2
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n : ℕ), 0 ≤ (fun n ↦ ↑K * b n) n

Tactic:
exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n : ℕ), 0 ≤ (fun n ↦ ↑K * b n) n

Tactic:
exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
symm_symm

Goal state after:
i j : ↑I
⊢ j ≤ σ i ↔ j ≤ σ i
Module: Mathlib.Topology.UnitInterval

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

Tactic:
symm_symm

Goal state after:
i j : ↑I
⊢ σ j ≤ i ↔ σ j ≤ i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ (σ j) < σ i ↔ j < σ i

Tactic:
symm_symm

Goal state after:
i j : ↑I
⊢ j < σ i ↔ j < σ i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ j < σ (σ i) ↔ σ j < i

Tactic:
symm_symm

Goal state after:
i j : ↑I
⊢ σ j < i ↔ σ j < i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type ?u.3
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
δ : α
s t : ↑unitInterval
⊢ ↑s * (1 - ↑t) / (1 - ↑s * ↑t) ≤ 1

Tactic:
by
      apply div_le_one_of_le₀
      · nlinarith [s.2.2]
      · nlinarith [s.2.2, t.2.2, t.2.1]

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

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

Tactic:
rw [lt_min_iff] at H

Goal state after:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ False
Module: Mathlib.Topology.MetricSpace.Polish

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

Tactic:
rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩

Goal state after:
case refine_4.refine_1
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
intro h i hi

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x

Tactic:
have hx : x.1 ≤ m := le_max_left _ _

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: 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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
⊢ ∃ y ∈ s, x ∈ cylinder y (Nat.find A - 1)

Tactic:
simpa only [not_disjoint_iff, mem_cylinder_comm] using Nat.find_min A B

Goal state after:
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) μ
B : ∀ (m : ℕ), μ (f^[m] ⁻¹' s) = μ s
this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
wlog hlt : i < j generalizing i j

Goal state after:
case inr
α : 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
this✝ : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
this : ∀ i < n, ∀ j < n, i ≠ j → f^[i] x ∈ s → f^[j] x ∈ s → i < j → ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
hlt : ¬i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

α : 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
this : μ univ < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: 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
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
this : firstDiff x y ≤ firstDiff (f x) (f y)
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ s ≤ 1

Tactic:
by
  apply (measure_mono (subset_univ _)).trans
  rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h <;> simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
inst✝ : IsProbabilityMeasure (map f μ)
hf : AEMeasurable f μ
⊢ (map f μ) univ = 1

Tactic:
exact IsProbabilityMeasure.measure_univ

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ ξ s = 0

Tactic:
← inter_union_compl s h.nullSet,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ ξ (s ∩ h.nullSet ∪ s ∩ h.nullSetᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ s.indicator 1 b

Tactic:
exact measurable_one.indicator hs

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ ↦ ∫⁻ (x : α), f x ∂μ

Tactic:
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
  refine .iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_
  refine Measurable.const_mul ?_ _
  exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x, f x * μ {x}

Tactic:
rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ ν.join = (id ν).bind id

Tactic:
exact join_eq_bind ν

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
n : ℕ
this : μ (K n) = 0
⊢ IsNowhereDense (K n)

Tactic:
exact .of_isClosed_null (hcompact n).isClosed this

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
n : ℕ
⊢ cylinder y n = cylinder (↑(p n)).2.2 (↑(p n)).1

Tactic:
rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
      intro i hi
      rw [hy]
      exact (Iy i n hi).symm

Goal state after:
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 ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
inter_comm,

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 (Subtype.val ⁻¹' s) ↔ MeasurableSet (range f ∩ s)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (⇑f.symm '' A)
U : Set α
hAU : U ⊇ ⇑f.symm '' A
hUo : IsOpen[inst✝⁵] U
hU : μ U < r
this : IsOpen[inst✝²] (⇑f.symm ⁻¹' U)
⊢ (map (⇑f) μ) (⇑f.symm ⁻¹' U) < r

Tactic:
rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]

Goal state after:
Module: Mathlib.GroupTheory.Complement

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

Tactic:
by
  have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_
  · ext
    · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
    · rw [this]
  · simp [RightCosetEquivalence, ← smul_smul]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
⊢ (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
have h_eq (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ}
      (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u) :
      ν.map MeasurableEquiv.prodAssoc (s ×ˢ (t ×ˢ u)) = ν ((s ×ˢ t) ×ˢ u) := by
    rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]
    congr 1 with x
    simp [MeasurableEquiv.prodAssoc]

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
⊢ (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)) ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : μ K ≠ 0
⊢ μ.IsOpenPosMeasure

Tactic:
refine ⟨fun U hU hne => ?_⟩

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : μ K ≠ 0
U : Set G
hU : IsOpen[inst✝⁴] U
hne : U.Nonempty
⊢ μ U ≠ 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ (map Prod.swap ρ).fst = ρ.snd

Tactic:
Measure.fst,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map Prod.fst (map Prod.swap ρ) = ρ.snd
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'

Goal state after:
α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed[w✝] s
right✝ : IsOpen[w✝] s
⊢ StandardBorelSpace ↑s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬μ univ = 0

Tactic:
MeasurableSet.univ.measure_eq_iSup_isCompact,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬⨆ K, ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), μ K = 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (L (n + 1)) = μ (L n) + μ (g (L n) • K)

Tactic:
by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet

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

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (c : ℝ≥0∞), μ K < c → ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U < c

Tactic:
simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
by
  ext1 t ht
  rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs),
    restrict_restrict ht]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ≠ 0 ↔ 0 < x

Tactic:
← not_le,

Goal state after:
x : ℝ
⊢ √x ≠ 0 ↔ ¬x ≤ 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ι : Type u_2
f g : ι → ℝ
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
⊢ ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)

Tactic:
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))

Goal state after: