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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∉ t
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

pp: case pos
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
· rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]
      exact tendsto_const_nhds

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
⊢ f n a ≤ f (n + 1) a

Tactic:
have := Set.notMem_subset hs.1 h

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
this : a ∉ {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a}
⊢ f n a ≤ f (n + 1) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), ⨅ n, (f ∘ Directed.sequence f h_directed) n a ∂μ =
    ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
⊢ StronglyMeasurable f

Tactic:
borelize β
  cases h.out
  · rw [stronglyMeasurable_iff_measurable_separable]
    refine ⟨hf.measurable, ?_⟩
    exact isSeparable_range hf
  · exact hf.measurable.stronglyMeasurable

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
x : α
hx : x ∉ s
n : ℕ
⊢ ((fun n ↦ (hf.approx n).restrict s) n) x = 0

Tactic:
simp [SimpleFunc.coe_restrict, hs, hx]

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst✝] U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
apply (hC _ xC).nhds_inter

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst✝] U
x : α
xU : x ∈ U
xC : x ∈ C
⊢ U ∈ 𝓝 x
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : AccPt y (𝓟 C)
⊢ ∃ x ∈ C, x ≠ y

Tactic:
rw [accPt_iff_nhds] at this

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
⊢ ∃ x ∈ C, x ≠ y
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2
α : 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 : ℕ
⊢ IsSeparable (range fun p ↦ u (↑p.1) p.2)

Tactic:
· have : IsSeparable (⋃ i : (t_sf n).range, range (u i)) :=
        .iUnion fun i => (h i).isSeparable_range
      apply this.mono
      rintro _ ⟨⟨i, x⟩, rfl⟩
      simp only [mem_iUnion, mem_range]
      exact ⟨i, x, rfl⟩

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ 0 ≤ 1 - ↑x

Tactic:
simpa using x.2.2

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

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
⊢ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩

Goal state after:
case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
⊢ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < min (min δX δY) ε → (a, b) ∈ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ cylinder y n = cylinder x n

Tactic:
by
  constructor
  · intro hy
    apply Subset.antisymm
    · intro z hz i hi
      rw [← hy i hi]
      exact hz i hi
    · intro z hz i hi
      rw [hy i hi]
      exact hz i hi
  · intro h
    rw [← h]
    exact self_mem_cylinder _ _

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

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ cylinder x n = cylinder y n

Tactic:
rw [← mem_cylinder_iff_eq]

Goal state after:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ x ∈ cylinder y n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ i < n + 1, y i = update x n k i
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)

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

Goal state before:
pp: case mp.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist ⟨i, x⟩ ⟨j, y⟩ < min ε 1
hij : i ≠ j
⊢ ⟨j, y⟩ ∈ s

Tactic:
apply (lt_irrefl (1 : ℝ) _).elim

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : ⟨i, x⟩ ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist ⟨i, x⟩ ⟨j, y⟩ < min ε 1
hij : i ≠ j
⊢ 1 < 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case refine_3.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
apply (lt_irrefl (1 : ℝ) _).elim

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ 1 < 1
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsOpen[inst✝¹] s
⊢ IsClopenable s

Tactic:
simpa using hs.isClosed_compl.isClopenable.compl

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

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ CompleteSpace ((n : ℕ) → E n)

Tactic:
refine Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) ?_

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (u : ℕ → (n : ℕ) → E n),
    (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N) → ∃ x, Tendsto u atTop (𝓝 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
x : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder y n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
exact mem_cylinder_iff_dist_le.1 hy

Goal state after:
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
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : longestPrefix x s < n
⊢ Disjoint s (cylinder x n)

Tactic:
contrapose! hn

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
n : ℕ
hn : ¬Disjoint s (cylinder x n)
⊢ n ≤ longestPrefix 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
⊢ cylinder x (firstDiff x y) = cylinder y (firstDiff x y)

Tactic:
rw [← mem_cylinder_iff_eq]

Goal state after:
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
⊢ x ∈ cylinder y (firstDiff x y)
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)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
⊢ cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y)

Tactic:
rw [← mem_cylinder_iff_eq]

Goal state after:
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)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = A.some
⊢ A.some ∈ cylinder x (firstDiff x y)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
⊢ map (fun x ↦ c) μ = μ univ • dirac c

Tactic:
by
  ext s hs
  simp only [Measure.coe_smul, Pi.smul_apply,
    dirac_apply' _ hs, smul_eq_mul]
  classical
  rw [Measure.map_apply measurable_const hs, Set.preimage_const]
  by_cases hsc : c ∈ s
  · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
  · rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]

Goal state after:
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)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y)

Tactic:
rw [← mem_cylinder_iff_eq]

Goal state after:
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)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ Ax.some ∈ cylinder x (firstDiff x y)
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
⊢ edist x y ≤ ∑' (i : ?m.10), 2⁻¹ ^ encode i

Tactic:
edist_eq_tsum

Goal state after:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EDist (F i)
x y : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (y i)) ≤ ∑' (i : ?m.10), 2⁻¹ ^ encode i
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rcases exists_measurable_le_lintegral_eq (join m) f with ⟨g, hgm, hgf, hfg_int⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
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 (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ∞

Tactic:
rw [prod_apply hs] at h2s
  exact ae_lt_top (measurable_measure_prodMk_left hs) h2s

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: 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

Tactic:
exact ⟨x.1, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (y, ⟨_, hy⟩)).1⟩

Goal state after:
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
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
m n : ℕ
⊢ (↑(s m) ∩ ↑(s n)).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter]

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
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
m n : ℕ
⊢ ¬Disjoint ↑(s m) ↑(s n)
Module: Mathlib.MeasureTheory.Group.Action

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

Tactic:
simpa [inv_inv] using (measure_symmDiff_inv_smul _ c⁻¹ _ _).symm

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

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
⊢ [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ].TFAE

Tactic:
tfae_have 5 → 3 := fun H c s _ => H c s

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
tfae_5_to_3 : (∀ (c : G) (s : Set α), μ (c • s) = μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
⊢ [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ].TFAE
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod ν = map (Prod.mk x) ν

Tactic:
by
  classical
  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]

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 ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (ν + ν') = μ.prod ν + μ.prod ν'

Tactic:
by
  simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum,
    sum_add_sum]
  congr
  ext1 i
  refine prod_eq fun s t _ _ => ?_
  simp_rw [add_apply, prod_prod, left_distrib]

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

Goal state before:
pp: case f_inj
γ : Type u_3
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
β : Type u_4
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst✝⁵] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace ↑s
⊢ Injective fun x ↦ f ↑x

Tactic:
· rwa [injOn_iff_injective] at f_inj

Goal state after: