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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n
hs_univ : ⋃ i, s i = univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ ↑n
⊢ ‖f x‖ ≤ ↑n

Tactic:
← coe_nnnorm

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n
hs_univ : ⋃ i, s i = univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ ↑n
⊢ ↑‖f x‖₊ ≤ ↑n
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ∞
⊢ False

Tactic:
refine absurd h_zero_top (ne_of_lt ?_)

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ∞
⊢ μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
n : ℕ
⊢ Measurable (g' n)

Tactic:
induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: E : Type u_3
inst✝ : SeminormedAddCommGroup E
ι : Type u_6
f : ι → E
⊢ ∑' (i : ι), ‖f i‖ₑ ≠ ∞ ↔ Summable fun i ↦ ‖f i‖

Tactic:
by
  simp only [tsum_enorm_ne_top_iff_summable_nnnorm, ← coe_nnnorm, NNReal.summable_coe]

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

Goal state before:
pp: E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ cylinder x 0 = univ

Tactic:
by simp [cylinder_eq_pi]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z

Tactic:
simp_all only [div_zero, sub_zero, one_mul, zero_mul, add_zero]
    replace hxy : (x : ℝ) ≤ (y : ℝ) := hxy
    replace hyz : (y : ℝ) ≤ (z : ℝ) := hyz
    linarith

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀
ht : ∀ (i : ι), ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = t i
⊢ ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i

Tactic:
choose u hcomp hcount hut using ht

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀
u : ι → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
hut : ∀ (i : ι), (u i).toTopologicalSpace = t i
⊢ ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩

Tactic:
rcases eq_or_ne j k with (rfl | hjk)
      · simp only [Sigma.dist_ne hij, Sigma.dist_same]
        calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel
      · simp only [hik, hij, hjk, Sigma.dist_ne, Ne, not_false_iff]
        calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
              dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
            simp only [add_zero, zero_add]
          _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]

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

Goal state before:
pp: case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F).pi U
Uu : (↑F).pi U ⊆ u
⊢ ∃ v ∈ {s | ∃ x n, s = cylinder x n}, x ∈ v ∧ v ⊆ u

Tactic:
rcases Finset.bddAbove F with ⟨n, hn⟩

Goal state after:
case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
u : Set ((n : ℕ) → E n)
hx : x ∈ u
u_open : IsOpen[Pi.topologicalSpace] u
U : (i : ℕ) → Set (E i)
F : Finset ℕ
xU : x ∈ (↑F).pi U
Uu : (↑F).pi U ⊆ u
n : ℕ
hn : n ∈ upperBounds ↑F
⊢ ∃ v ∈ {s | ∃ x n, s = cylinder x n}, x ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
intro u

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)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
refine ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
i : ℕ
⊢ Tendsto (fun i_1 ↦ u i_1 i) atTop (𝓝 (u i i))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
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 : y ∈ cylinder x n
⊢ False

Tactic:
apply lt_irrefl (infDist x s)

Goal state after:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
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 : y ∈ cylinder x n
⊢ infDist x s < infDist x s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff x y
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s

Tactic:
rw [firstDiff_comm] at H

Goal state after:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x y : (n : ℕ) → E n
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
H : longestPrefix x s < firstDiff y x
xs : x ∉ s
ys : y ∉ s
L : longestPrefix y s < longestPrefix x s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
Z : Disjoint s (cylinder y (longestPrefix x s))
⊢ longestPrefix y s = longestPrefix x s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
⊢ AnalyticSet (range f)

Tactic:
cases isEmpty_or_nonempty β
  · rw [range_eq_empty]
    exact analyticSet_empty
  · rw [AnalyticSet]
    obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
      exists_nat_nat_continuous_surjective β
    refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩
    rw [hg.range_comp]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ ↔ μ = 0

Tactic:
refine ⟨?_, fun h ↦ by (rw [h]; exact zero_left)⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ → μ = 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
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
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
have fy : f y = Ay.some := by simp_rw [f, if_neg ys]

Goal state after:
case neg
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
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
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 : longestPrefix y s < firstDiff x y
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)

Tactic:
rw [firstDiff_comm] at H

Goal state after:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
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 : longestPrefix y s < firstDiff y x
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
this : ⊥ = 0
u : Set α
hu : MeasurableSet u
x✝ : u.Nonempty
⊢ (μ ⊓ ν) u ≤ ⊥ u

Tactic:
simp only [Measure.inf_apply hu, this, coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
this : ⊥ = 0
u : Set α
hu : MeasurableSet u
x✝ : u.Nonempty
⊢ sInf {m | ∃ t, m = μ (t ∩ u) + ν (tᶜ ∩ u)} = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a

Tactic:
by
  ext s
  simp [mem_ae_iff, imp_false]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑(#(Finset.image f s)) = count ↑s

pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)

Tactic:
count_apply_finset' s_mble,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑(#(Finset.image f s)) = ↑(#s)

α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
⊢ MeasurableSet A → (x ∈ A ↔ y ∈ A)

Tactic:
A_mble

Goal state after:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
n m : ι
⊢ Disjoint (t n) (⋂ n, u m n)

Tactic:
apply Disjoint.mono_right _ (htu m n)

Goal state after:
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
n m : ι
⊢ ⋂ n, u m n ⊆ u m n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α), f x ∂μ < ∞

Tactic:
← μ.restrict_univ

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ ↦ μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Tactic:
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 α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i ≤ ↑c

Tactic:
convert! ENNReal.coe_le_coe.mpr tsum_le_c

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i = ↑(∑' (i : α), a i)
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, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous f

Tactic:
apply exists_retraction_subtype_of_isClosed s_closed
    simpa only [nonempty_coe_sort] using g_surj.nonempty

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ

Tactic:
calc
    (ψ.map (↑)).lintegral (μ.restrict s) = ∫⁻ a in s, ψ a ∂μ :=
      SimpleFunc.lintegral_eq_lintegral .. |>.symm
    _ ≤ ∫⁻ a in s, min (f a) n ∂μ :=
      lintegral_mono fun a ↦ le_min (hψ _) (ENNReal.coe_le_coe.2 (hn a))
    _ ≤ ∫⁻ a in s, g n a ∂μ := by
      have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)
    _ ≤ _ := lintegral_mono fun x ↦ le_iSup (g · x) n

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

Goal state before:
pp: case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
refine continuous_projIcc.comp <| Continuous.dist continuous_id' ?_

Goal state after:
case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun x ↦ denseSeq X n
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x y : X
hxy : x ≠ y
⊢ ∃ n, distDenseSeq X n x ≠ distDenseSeq X n y

Tactic:
obtain ⟨n, hn⟩ := separation ((isOpen_compl_singleton (x := y)).mem_nhds hxy)

Goal state after:
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x y : X
hxy : x ≠ y
n : ℕ
hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
⊢ ∃ n, distDenseSeq X n x ≠ distDenseSeq X n y
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ ↑(hST.equiv g).1 = ↑⟨1, h1⟩

Tactic:
equiv_fst_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ g * (↑(hST.equiv g).2)⁻¹ = ↑⟨1, h1⟩
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.fst
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)).1 = ↑h * ↑(hHT.equiv g).1

Tactic:
equiv_fst_eq_mul_inv,

Goal state after:
case refine_2.fst
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
⊢ ↑h * g * (↑(hHT.equiv (↑h * g)).2)⁻¹ = ↑h * ↑(hHT.equiv g).1
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.fst
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
⊢ ↑h * g * (↑(hHT.equiv g).2)⁻¹ = ↑h * ↑(hHT.equiv g).1

Tactic:
equiv_fst_eq_mul_inv,

Goal state after:
case refine_2.fst
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
⊢ ↑h * g * (↑(hHT.equiv g).2)⁻¹ = ↑h * (g * (↑(hHT.equiv g).2)⁻¹)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ ↑(hST.equiv g).1 = 1 ↔ g ∈ T

Tactic:
equiv_fst_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g * (↑(hST.equiv g).2)⁻¹ = 1 ↔ g ∈ T
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv (f • f⁻¹ • q))

Tactic:
smul_inv_smul

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = ↑(⋯.leftQuotientEquiv q)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ ∀ (i : Set α), k ⊆ i → IsOpen[inst✝²] i → μ (closure[inst✝²] k) ≤ μ i

Tactic:
intro u

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
⊢ k ⊆ u → IsOpen[inst✝²] u → μ (closure[inst✝²] k) ≤ μ u