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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ y ∈ s ×ˢ t, max (edist x.1 y.1) (edist x.2 y.2) = max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)

Tactic:
iInf_prod,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ ⨅ i, ⨅ j, ⨅ (_ : (i, j) ∈ s ×ˢ t), max (edist x.1 (i, j).1) (edist x.2 (i, j).2) =
    max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ max (⨆ x ∈ s, infEDist x u) (⨆ y ∈ u, infEDist y s) ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ (∀ i ∈ s, infEDist i u ≤ hausdorffEDist s t + hausdorffEDist t u) ∧
    ∀ i ∈ u, infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
⊢ hausdorffEDist {x} {y} = edist x y

Tactic:
simp_rw [hausdorffEDist, iSup_singleton, infEDist_singleton]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
⊢ max (edist x y) (edist y x) = edist x y
Module: Mathlib.Topology.MetricSpace.Thickening

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

Tactic:
by
  simp_rw [thickening, infEDist_closure]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
h : a < b
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

pp: case inr
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
h : b ≤ a
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
· have : a < b + c := h.trans_le (le_self_add ..)
    tauto

Goal state after:
case inr
α : Type u_1
inst✝⁴ : LinearOrder α
a b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
h : b ≤ a
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)

Tactic:
simp_rw [lt_add_iff_lt_left_or_exists_lt]

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < b ∨ ∃ d < c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)

Tactic:
simp_rw [lt_add_iff_lt_left_or_exists_lt]

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < b ∨ ∃ d < c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

Tactic:
simp_rw [le_add_iff_lt_right_or_exists_le]
  aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)

Tactic:
simp_rw [le_add_iff_lt_right_or_exists_le]
  aesop

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case mp
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
by_cases hq : q
    · simp only [hq, ite_true] at h
      filter_upwards [mem_map.mp (h hbF)] with i hi
      simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_right_iff, not_forall, exists_prop] at hi
      tauto
    · simp only [hq, ite_false] at h
      filter_upwards [mem_map.mp (h haG)] with i hi
      simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_left_iff, not_forall, exists_prop] at hi
      tauto

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

Goal state before:
pp: case inl
α : 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 : IsEmpty (Subtype p)
⊢ Measurable fun x ↦ liminf (fun x_1 ↦ f x_1 x) v

Tactic:
simp [hv.liminf_eq_sSup_iUnion_iInter]

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ → ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞

pp: case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞) → f.FinMeasSupp μ

Tactic:
· refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h
    exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞) → f.FinMeasSupp μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
h : Measurable fun x ↦ ↑(f x)
⊢ Measurable f

Tactic:
by simpa only [Real.toNNReal_coe] using h.real_toNNReal

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
h : AEMeasurable (fun x ↦ ↑(f x)) μ
⊢ AEMeasurable f μ

Tactic:
by simpa only [Real.toNNReal_coe] using h.real_toNNReal

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
⊢ x ∉ ↑s

Tactic:
rwa [Finset.mem_coe]

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

Goal state before:
pp: case refine_2
α✝ : 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:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Goal state before:
pp: case refine_3
α✝ : 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:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Goal state before:
pp: case refine_4
α✝ : 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

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Tactic:
exact (measurable_const_mul _).comp measurable_coe_real_ereal

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

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x ↦ 1) μ
⊢ AEMeasurable (A.indicator fun x ↦ 1) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L As_mble

Goal state after:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x ↦ 1) μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ (As n).indicator (fun x ↦ 1) x) L (𝓝 (A.indicator (fun x ↦ 1) x))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
⊢ x ∉ ↑s

Tactic:
rwa [Finset.mem_coe]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : f =ᵐ[μ.restrict s] AEStronglyMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
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
h : ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → (fs m) x = (f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), n₂ ≤ b → (f_approx b) x ∈ s
m : ℕ
hm : max n₁ n₂ ≤ m
⊢ (fs m) x ∈ s

Tactic:
rw [hn₁ m ((le_max_left _ _).trans hm)]

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 : ∀ s ∈ 𝓝 (f x), ∃ a, ∀ (b : ℕ), a ≤ b → (f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → (fs m) x = (f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), n₂ ≤ b → (f_approx b) x ∈ s
m : ℕ
hm : max n₁ n₂ ≤ m
⊢ (f_approx m) x ∈ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : ¬u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
· simp_all

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : α → ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ ∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ

Tactic:
simp only [lintegral_def, iSup_comm (ι := ι),
    SimpleFunc.lintegral_restrict_iUnion_of_directed _ hd]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), limsup (fun n ↦ f n a) atTop ∂μ

Tactic:
by simp only [limsup_eq_iInf_iSup_of_nat]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ b ∈ insert a s, AEMeasurable (f b) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
rw [Finset.forall_mem_insert] at hf

Goal state after:
case insert
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : (∀ b ∈ s, AEMeasurable (f b) μ) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
⊢ ∀ (n : ℕ), μ (support ⇑(0 n)) < ∞

Tactic:
simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero, measure_empty,
      zero_lt_top, forall_const]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
    Measure.restrict_eq_zero.mpr h, add_zero]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩

Goal state after:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case a
α : 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∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ

Tactic:
rw [hg n]
      exact lintegral_mono (I n)

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

Goal state before:
pp: case inl
α : 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 ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : Tendsto (fun i ↦ f i a) atTop atBot
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
refine ⟨0, h.mono_right ?_⟩
      rw [OrderBot.atBot_eq]
      exact pure_le_nhds _

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
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)

pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)

Tactic:
· simp_all

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)
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 - ↑x) / (↑z - ↑x) ≤ 1

pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ (↑y - ↑x) / (↑z - ↑x) ≤ 1

Tactic:
· simp_all

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ (↑y - ↑x) / (↑z - ↑x) ≤ 1
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ (s ∩ cylinder x (longestPrefix x s)).Nonempty

Tactic:
have B : longestPrefix x s < shortestPrefixDiff x s :=
    Nat.pred_lt (shortestPrefixDiff_pos hs hne hx).ne'

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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : longestPrefix x s < shortestPrefixDiff x s
⊢ (s ∩ cylinder x (longestPrefix x s)).Nonempty
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
y : (n : ℕ) → E n
hy : y ∉ s
⊢ f y ∈ s

Tactic:
simpa [f, if_neg hy] using! (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g) μ ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
by_cases ha : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ (∀ᵐ (b : β) ∂μ, f b ∈ s) ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a

Tactic:
← ae_map_iff hf (by measurability),

Goal state after:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ (∀ᵐ (y : α) ∂map f μ, y ∈ s) ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
rw [← lintegral_count] at tsum_le_c

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

Tactic:
by
  rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
    add_comm]
  rwa [disjoint_singleton_right]

Goal state after: