mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
⊢ Measurable fun x ↦ ⨅ i, f (↑i) x

Tactic:
have F0_meas : ∀ j, Measurable (F0 j) := fun j ↦ .iInf (fun (i : s j) ↦ hf i)

Goal state after:
case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this✝ : Countable (Subtype p)
hp : Nonempty (Subtype p)
H : ¬∃ j, s ↑j = ∅
this : ∀ (i : ι'), Countable ↑(s i)
m : Subtype p → Set δ := fun j ↦ {x | BddBelow (range fun i ↦ f (↑i) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun x ↦ liminfReparam (fun i ↦ f i x) s p
F0 : Subtype p → δ → α := fun j x ↦ ⨅ i, f (↑i) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
⊢ Measurable fun x ↦ ⨅ i, f (↑i) x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ ⋯.some) atTop (𝓝 ⋯.some)

Tactic:
· simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ ⋯.some) atTop (𝓝 ⋯.some)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : f p ≠ 0
⊢ p ∈ s

Tactic:
rw [← Function.mem_support] at H

Goal state after:
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∈ support f
⊢ p ∈ s
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᵐ[μ.trim hm₀] g
⊢ AEStronglyMeasurable f μ

Tactic:
exact ⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᵐ[μ.restrict sᶜ] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∈ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
simp [hxs, hx]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
rw [norm_eq_zero] at hfx0

Goal state after:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : f x = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ f a), g.lintegral μ =
    ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
refine
    le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ∞
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
let ψ := φ.map ENNReal.toNNReal
    replace h : ψ.map ((↑) : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono fun a => ENNReal.coe_toNNReal
    have : ∀ x, ↑(ψ x) ≤ f x := fun x => le_trans ENNReal.coe_toNNReal_le_self (hφ x)
    exact le_iSup₂_of_le (φ.map ENNReal.toNNReal) this (ge_of_eq <| lintegral_congr h)

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : ℕ → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : ℕ → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
⊢ ∀ᵐ (x : α) ∂μ, g x ∈ closure[inst✝³] (⋃ i, t i)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
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:
have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x

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
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ univ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
by
  by_cases hf₀ : ∫⁻ a, f a ∂μ = 0
  · exact ⟨∅, .empty, by simp, by simpa [hf₀, pos_iff_ne_zero]⟩
  obtain ⟨g, hgf, hg_meas, hgsupp, hgε⟩ :
      ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ a, f a ∂μ - ε < ∫⁻ a, g a ∂μ := by
    obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
      simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
    refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
    exact SimpleFunc.FinMeasSupp.of_lintegral_ne_top <| ne_top_of_le_ne_top hf <|
      g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf
  refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩
  calc
    ∫⁻ a in (support g)ᶜ, f a ∂μ
      = ∫⁻ a in (support g)ᶜ, f a - g a ∂μ := setLIntegral_congr_fun
      (measurableSet_support hg_meas).compl <| by intro; simp_all
    _ ≤ ∫⁻ a, f a - g a ∂μ := setLIntegral_le_lintegral _ _
    _ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
      lintegral_sub hg_meas (ne_top_of_le_ne_top hf <| lintegral_mono hgf) (ae_of_all _ hgf)
    _ < ε := ENNReal.sub_lt_of_lt_add (lintegral_mono hgf) <|
      ENNReal.lt_add_of_sub_lt_left (.inl hf) hgε

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl✝ : Tendsto x atTop l
xl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
⊢ ?m.61

Tactic:
exact xl

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

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
n : ℕ
⊢ ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ

Tactic:
exact hf_prop n

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ closure[inst✝¹] (U ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Goal state after:
case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ U ∩ C ⊆ C
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ closure[inst✝¹] (V ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Goal state after:
case h.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ V ∩ C ⊆ C
Module: Mathlib.Topology.MetricSpace.PiNat

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

Tactic:
rw [firstDiff_def] at hn
  aesop

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

Goal state before:
pp: case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

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

Goal state before:
pp: case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

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

Goal state before:
pp: case mp.inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))

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

Goal state before:
pp: case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)

Tactic:
rw [Filter.mem_map, mem_uniformity_dist]

Goal state after:
case mpr.left
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)

Tactic:
rw [Filter.mem_map, mem_uniformity_dist]

Goal state after:
case mpr.right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

Tactic:
rintro hs ⟨i, x⟩ hx
    obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
      Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
    refine ⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩
    rintro ⟨j, y⟩ hy
    rcases eq_or_ne i j with (rfl | hij)
    · simp only [Sigma.dist_same, lt_min_iff] at hy
      exact hε (mem_ball'.2 hy.1)
    · apply (lt_irrefl (1 : ℝ) _).elim
      calc
        1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
        _ < 1 := hy.trans_le (min_le_right _ _)

Goal state after:
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)
j : ℕ
y : X j
hy : ⟨j, y⟩.fst ≤ 0
x : X 0
hx : ⟨0, x⟩.fst ≤ 0
⊢ inductiveLimitDist f ⟨0, x⟩ ⟨j, y⟩ =
    dist (leRecOn hx (fun {k} ↦ f k) ⟨0, x⟩.snd) (leRecOn hy (fun {k} ↦ f k) ⟨j, y⟩.snd)

Tactic:
obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x : X 0
hx : ⟨0, x⟩.fst ≤ 0
y : X 0
hy : ⟨0, y⟩.fst ≤ 0
⊢ inductiveLimitDist f ⟨0, x⟩ ⟨0, y⟩ =
    dist (leRecOn hx (fun {k} ↦ f k) ⟨0, x⟩.snd) (leRecOn hy (fun {k} ↦ f k) ⟨0, y⟩.snd)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: 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)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ A (res x n)

Tactic:
apply hanti _ (x 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)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (A (x n :: res x n))
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case hfh.false
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
n : ℕ
hm : n.succ ≠ 0
⊢ ediam (D (false :: PiNat.res x n)) ≤ u (n + 1)

Tactic:
convert! (h0 _ _ _).2.2.2
      rw [PiNat.res_length]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
ν : Measure β
⊢ (m.bind fun x ↦ ν) = m univ • ν

Tactic:
by
  simp [bind]

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ ∑ i ∈ K, edist (x i) (y i) + ∑' (i : ↑(↑K)ᶜ), 2⁻¹ ^ encode ↑i < ∑ _i ∈ K, δ + ε / 2

Tactic:
refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed[inst✝³] F
⊢ μ F = μ univ ↔ F = univ

Tactic:
by
  rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]

Goal state after: