mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ (Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ range f)

Tactic:
← hf.map_apply,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ (Measure.map f (Measure.comap f μ)) s = μ (s ∩ range f)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
⊢ SigmaFinite μ ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => by infer_instance⟩

Goal state after:
α : Type u_1
μ : Measure α
h : SigmaFinite μ
⊢ μ univ < ∞
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
⊢ CountablySeparated α

Tactic:
by
  simp_rw [countablySeparated_def] at *
  rcases hsep with ⟨S, Sct, Smeas, hS⟩
  use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS

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

Goal state before:
pp: case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋂ i, ⋃ j, spanningSets (μ i) j = univ

Tactic:
iUnion_spanningSets,

Goal state after:
case intro.refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst✝¹ : Finite ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
val✝ : Fintype ι
this : ∀ (n : ℕ), MeasurableSet (⋂ i, spanningSets (μ i) n)
⊢ ⋂ i, univ = univ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
⊢ f ⁻¹' ⋃ i, spanningSets (Measure.map f μ) i = univ

Tactic:
iUnion_spanningSets,

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
⊢ f ⁻¹' univ = univ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ (f '' ⋃ i, spanningSets μ i) ∪ (range f)ᶜ = univ

Tactic:
iUnion_spanningSets,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst✝ : SigmaFinite μ
⊢ f '' univ ∪ (range f)ᶜ = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
⊢ generateFrom (⋃ n, memPartition t n) = generateFrom (range t)

Tactic:
refine le_antisymm (generateFrom_le fun u hu ↦ ?_) (generateFrom_le fun u hu ↦ ?_)

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ ⋃ n, memPartition t n
⊢ MeasurableSet u

case refine_2
α : Type u_1
t : ℕ → Set α
u : Set α
hu : u ∈ range t
⊢ MeasurableSet u
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
by
  nontriviality α; inhabit α
  obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
    h.exists_ae_eq_range_subset (Eventually.of_forall hfs) ⟨_, hfs default⟩
  refine ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, ?_⟩
  filter_upwards [fg] with x hx
  simpa [Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Group α
inst✝ : MeasurableDiv α
⊢ Measurable Inv.inv

Tactic:
simpa using measurable_const_div (1 : α)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEDist x E

Tactic:
← infEDist_pos_iff_notMem_closure,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : 0 < infEDist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEDist x E
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
⊢ infEDist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEDist x s ≤ r
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
rw [hausdorffEDist_zero_iff_closure_eq_closure, closure_closure]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ ν (Iic a) ≠ ∞

Tactic:
← h a

Goal state after:
case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
a b : α
hlt : a < b
⊢ μ (Iic a) ≠ ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
⊢ infDist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩

Goal state after:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g : δ → α
hf : ∀ (i : ι), Measurable (f i)
hg : ∀ (b : δ), IsLUB (range fun i ↦ f i b) (g b)
a : α
⊢ MeasurableSet (⋃ i, {x | a < f i x})

Tactic:
exact MeasurableSet.iUnion fun i => hf i (isOpen_lt' _).measurableSet

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
X : α → β
Y : α → γ
⊢ MeasurableSpace.comap (fun ω ↦ (X ω, Y ω)) (mβ.prod mγ) = MeasurableSpace.comap X mβ ⊔ MeasurableSpace.comap Y mγ

Tactic:
by
  simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
  rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
X : γ → α
Y : δ → β
⊢ MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)

Tactic:
by
  simp_rw [MeasurableSpace.prod, comap_sup, comap_comp]
  rfl

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case refine_3
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
x : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) x) L (𝓝 (A.indicator (fun x ↦ b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
convert! heart

Goal state after:
case e'_5
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
x : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ 𝓝 (A.indicator (fun x ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
a : ℝ≥0∞
ha✝ : a ∈ f.range
ha : a ≠ ∞
ha0 : a = 0
⊢ a * μ (⇑f ⁻¹' {a}) < ∞

Tactic:
subst a

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
ha✝ : 0 ∈ f.range
ha : 0 ≠ ∞
⊢ 0 * μ (⇑f ⁻¹' {0}) < ∞
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : 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))
⊢ AEMeasurable g μ

Tactic:
by
  classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_5
x✝ : MeasurableSpace α
ι : Type u_6
inst✝ : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ (∑' (b : ι), ↑(f b x)).toNNReal) μ

Tactic:
exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : 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)
F1 : δ → α := fun x ↦ F0 (reparam x j) x
hF1 : F1 = fun x ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose ⋯
Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find ⋯)
hjx : x ∈ m j
⊢ reparam x j = j

Tactic:
rw [A, if_pos hjx]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_5
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α✝
mα✝ : MeasurableSpace α✝
α : Type u_5
β : Type u_6
γ : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Measurable fun r ↦ (↑r, ⊤).1 * (↑r, ⊤).2

Tactic:
simp_rw [mul_comm _ ⊤]
    exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Goal state before:
pp: α : 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 β
⊢ AEStronglyMeasurable g μ

Tactic:
refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩

Goal state after:
case refine_1
α : 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 β
⊢ AEMeasurable g μ

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 β
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
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
b : β
⊢ ∫⁻ (a : α), f b a ∂μ ≤ ⨆ n, ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ

Tactic:
· exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), (eapprox f n) a ∂μ = (eapprox f n).lintegral μ

Tactic:
(eapprox f n).lintegral_eq_lintegral

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ (eapprox f n).lintegral μ = (eapprox f n).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Norm

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᵐ[μ] f
x : α
hx : 0 x ≤ f x
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)

Tactic:
rw [Real.enorm_eq_ofReal hx]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (⋃ i, spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) i) ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n

Tactic:
iUnion_spanningSets,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ Set.univ ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Module: Mathlib.Topology.Perfect

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

Tactic:
rintro x ⟨xU, xC⟩

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
⊢ AccPt x (𝓟 (U ∩ C))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
exact fun p => ht_sf p.fst p.snd

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

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun i ↦ U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
exact fun p => ht_sf p.fst p.snd

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)

Tactic:
glueDist,

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + ε)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n ⊆ cylinder x n

pp: case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n

Tactic:
· intro z hz i hi
      rw [← hy i hi]
      exact hz i hi

Goal state after:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

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

Goal state before:
pp: case 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
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩

Tactic:
rcases eq_or_ne i j with (rfl | hij)
    · simp only [Sigma.dist_ne hik, Sigma.dist_same]
      calc
        dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
            dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z := by
          apply_rules [add_le_add, le_rfl, dist_triangle]
        _ = _ := by abel
    · 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.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ ∀ (a : ↑(inducedMap A).fst),
    ∀ ε > 0, ∀ᶠ (x : ↑(inducedMap A).fst) in 𝓝 a, dist ((inducedMap A).snd x) ((inducedMap A).snd a) < ε

Tactic:
rintro x ε ε_pos

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 x, dist ((inducedMap A).snd x_1) ((inducedMap A).snd x) < ε
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑x) n)

Tactic:
rw [← hyx]
      apply map_mem

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

Goal state before:
pp: case refine_1
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
⊢ range f = s

Tactic:
apply Subset.antisymm
    · rintro x ⟨y, rfl⟩
      by_cases hy : y ∈ s
      · rwa [fs y hy]
      simpa [f, if_neg hy] using! (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1
    · intro x hx
      rw [← fs x hx]
      exact mem_range_self _

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

Goal state before:
pp: case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous[_, inst✝] f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

Tactic:
exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩

Goal state after: