mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : AccPt x (𝓟 (closure[inst✝¹] C))
⊢ AccPt x (𝓟 C)

Tactic:
accPt_iff_frequently

Goal state after:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure[inst✝¹] C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure[inst✝¹] C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_1
α : 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
⊢ IsClosed[inst✝¹] D

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
⊢ Preperfect D

pp: case refine_3
α : 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
⊢ C = V ∩ C ∪ D

Tactic:
· refine hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)
    exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub

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
⊢ Preperfect D

case refine_3
α : 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
⊢ C = V ∩ C ∪ D
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : 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 m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ ↑K * dist (u n) (u m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2

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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.MetricSpace.Polish

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

Tactic:
iInf_uniformity

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

Goal state before:
pp: case succ
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ ¬_root_.Disjoint (A (↑x n :: res (↑x) n)) (A (↑y n :: res (↑x) n))

Tactic:
not_disjoint_iff

Goal state after:
case succ
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ ∃ x_1 ∈ A (↑x n :: res (↑x) n), x_1 ∈ A (↑y n :: res (↑x) n)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ n, ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε

Tactic:
use n

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
I : ∀ (n : ℕ), 1 / C ≤ infDist (↑(u n)) (↑s)ᶜ
⊢ ∃ x, Tendsto u atTop (𝓝 x)

Tactic:
have I' : 1 / C ≤ infDist x sᶜ :=
    have : Tendsto (fun n => infDist (u n).1 sᶜ) atTop (𝓝 (infDist x sᶜ)) :=
      ((continuous_infDist_pt (sᶜ : Set α)).tendsto x).comp xlim
    ge_of_tendsto' this I

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
I : ∀ (n : ℕ), 1 / C ≤ infDist (↑(u n)) (↑s)ᶜ
I' : 1 / C ≤ infDist x (↑s)ᶜ
⊢ ∃ x, Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Tactic:
use n

Goal state after:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∀ m ≥ n, ∀ n_1 ≥ n, dist (u m) (u n_1) < ε
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ closure (eball x (ε / 2) ∩ C) ⊆ C

Tactic:
IsClosed.closure_subset_iff hC.closed

Goal state after:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ eball x (ε / 2) ∩ C ⊆ C
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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A ≤ firstDiff x y
⊢ (s ∩ cylinder x (Nat.find A)).Nonempty

Tactic:
refine ⟨y, hy, ?_⟩

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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A ≤ firstDiff x y
⊢ y ∈ cylinder x (Nat.find A)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
by
  tfae_have 1 → 2
  | h => h.disjoint
  tfae_have 2 → 1
  | h => mutuallySingular_of_disjoint h
  tfae_have 1 → 3
  | h => h.disjoint_ae
  tfae_have 3 → 2
  | h => disjoint_of_disjoint_ae h
  tfae_finish

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ measurableAtom y = s

Tactic:
rw [← hz, ← hsy]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
x y : α
s : Set α
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
h1 : measurableAtom y = measurableAtom x
z : α
left✝ : z ∈ univ
hz : measurableAtom z = s
h_points_mem : points ⟨s, ⋯⟩ ∈ s
hsy : points ⟨s, ⋯⟩ = y
⊢ measurableAtom (points ⟨s, ⋯⟩) = measurableAtom z
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
rw [count_apply_infinite hs]
    rw [← finite_image_iff hf.injOn] at hs
    rw [count_apply_infinite hs]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ

Tactic:
biUnion_of_singleton

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m

Tactic:
clear hf

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Dense {x | p x}

Tactic:
by
  rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]
  exact μ.interior_eq_empty_of_null hp

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: 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
y : ↑S
hy : (fun s ↦ (↑s)⁻¹ * g ∈ T) y
⊢ ?m.180 = ?m.181

Tactic:
simpa using hx' (y, ⟨_, hy⟩)

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_left 1

Goal state after:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
⊢ μ.OuterRegular

Tactic:
refine ⟨fun A hA r hr => ?_⟩
  have HA : μ A < ∞ := lt_of_lt_of_le hr le_top
  have hm : ∀ n, MeasurableSet (s n) := fun n => (h' n).measurableSet
  -- Note that `A = ⋃ n, A ∩ disjointed s n`. We replace `A` with this sequence.
  obtain ⟨A, hAm, hAs, hAd, rfl⟩ :
    ∃ A' : ℕ → Set α,
      (∀ n, MeasurableSet (A' n)) ∧
        (∀ n, A' n ⊆ s n) ∧ Pairwise (Disjoint on A') ∧ A = ⋃ n, A' n := by
    refine
      ⟨fun n => A ∩ disjointed s n, fun n => hA.inter (MeasurableSet.disjointed hm _), fun n =>
        inter_subset_right.trans (disjointed_subset _ _),
        (disjoint_disjointed s).mono fun k l hkl => hkl.mono inf_le_right inf_le_right, ?_⟩
    rw [← inter_iUnion, iUnion_disjointed, univ_subset_iff.mp h'', inter_univ]
  rcases ENNReal.exists_pos_sum_of_countable' (tsub_pos_iff_lt.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩
  rw [lt_tsub_iff_right, add_comm] at hδε
  have : ∀ n, ∃ U ⊇ A n, IsOpen U ∧ μ U < μ (A n) + δ n := by
    intro n
    have H₁ : ∀ t, μ.restrict (s n) t = μ (t ∩ s n) := fun t => restrict_apply' (hm n)
    have Ht : μ.restrict (s n) (A n) ≠ ∞ := by
      rw [H₁]
      exact ((measure_mono (inter_subset_left.trans (subset_iUnion A n))).trans_lt HA).ne
    rcases (A n).exists_isOpen_lt_add Ht (δ0 n).ne' with ⟨U, hAU, hUo, hU⟩
    rw [H₁, H₁, inter_eq_self_of_subset_left (hAs _)] at hU
    exact ⟨U ∩ s n, subset_inter hAU (hAs _), hUo.inter (h' n), hU⟩
  choose U hAU hUo hU using this
  refine ⟨⋃ n, U n, iUnion_mono hAU, isOpen_iUnion hUo, ?_⟩
  calc
    μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
    _ ≤ ∑' n, (μ (A n) + δ n) := ENNReal.tsum_le_tsum fun n => (hU n).le
    _ = ∑' n, μ (A n) + ∑' n, δ n := ENNReal.tsum_add
    _ = μ (⋃ n, A n) + ∑' n, δ n := (congr_arg₂ (· + ·) (measure_iUnion hAd hAm).symm rfl)
    _ < r := hδε

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 → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
rw [← MeasurableEquiv.prodAssoc.map_measurableEquiv_injective.eq_iff, ext_prod₃_iff]
  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]
  refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩ <;> specialize h hs ht hu
  · rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at h
  · rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ (μ.restrict (toMeasurable μ (s ∩ A))) K = (μ.restrict (s ∩ A)) K

Tactic:
rwa [restrict_toMeasurable]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (fun x ↦ (x, y)) (sfiniteSeq μ i)) (s ×ˢ t) = (sfiniteSeq μ i) s * (dirac y) t

Tactic:
map_apply measurable_prodMk_right (hs.prod ht),

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq μ i) ((fun x ↦ (x, y)) ⁻¹' s ×ˢ t) = (sfiniteSeq μ i) s * (dirac y) t
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ c • Measure.map (fun x ↦ g * x) μ = c • μ

Tactic:
map_mul_left_eq_self

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
⊢ c • μ = c • μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
by_cases hY : AEMeasurable Y μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ μ F = ⨆ n, μ (F ∩ B n)

Tactic:
rw [← Monotone.measure_iUnion, hBU]

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ Monotone fun n ↦ F ∩ B n
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ g * x) μ = μ

Tactic:
map_mul_left_eq_self

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

Goal state before:
pp: x y : ℝ
h : x ≤ y
⊢ NNReal.sqrt x.toNNReal ≤ NNReal.sqrt y.toNNReal

Tactic:
NNReal.sqrt_le_sqrt

Goal state after:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
⊢ NormedAddGroupHom.comp 0 f = 0

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
⊢ (incl g.ker).comp (lift f g h) = f

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x u : R
hu : u ∈ unitary R
⊢ Commute u x ↔ star u * x * u = x

Tactic:
simpa using! (Unitary.toUnits ⟨u, hu⟩).commute_iff_inv_mul_cancel

Goal state after: