mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
⊢ (∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i) → ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i

Tactic:
· rintro ⟨p, hpq, hpx⟩ p' hqp' hx_mem
      have hpp' : p ≠ p' := by grind
      have h_disj : Disjoint (countablyGeneratedAtom α p) (countablyGeneratedAtom α p') :=
        disjoint_countablyGeneratedAtom hpp'
      grind

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
rw [countablySeparated_def]
  exact HasCountableSeparatingOn.subtype_iff

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, univ = univ

Tactic:
iInter_univ

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' f '' {x})

Tactic:
image_singleton

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
⊢ sum f = f true + f false

Tactic:
rw [sum_fintype, Fintype.sum_bool]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Tactic:
map_apply_of_aemeasurable (M _) hs

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

Goal state before:
pp: case zero
α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁴ : MeasurableSpace M✝
inst✝³ : MeasurableSMul M✝ X
M : Type u_6
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable fun x ↦ (x, 0).2 • (x, 0).1

Tactic:
simp only [zero_smul, ← Pi.zero_def, measurable_zero]

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

Goal state before:
pp: γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
apply measurable_of_isOpen; intro s hs
  rw [← MeasurableSet.compl_iff, ← preimage_compl]; apply hf; rw [isClosed_compl_iff]; exact hs

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

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

Tactic:
refine le_antisymm (infEDist_anti subset_closure) ?_
  refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_
  have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
  have : infEDist x (closure s) < infEDist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'
  obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEDist x (closure s) + ↑ε / 2⟩ :=
    infEDist_lt_iff.mp this
  obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0
  calc
    infEDist x s ≤ edist x z := infEDist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEDist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEDist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

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

Goal state before:
pp: α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α

Tactic:
by
  apply generateFrom_le
  borelize α
  rintro _ ⟨a, -, b, -, -, rfl⟩
  exact measurableSet_Ico

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

Goal state before:
pp: case h₂
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst✝³] t
u : Set α
u_open : IsOpen[inst✝⁶] u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (u ∩ sᶜ)

Tactic:
exact u_open.measurableSet.inter hs.compl

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

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inl.inl
α : Type u
inst✝ : PseudoEMetricSpace α
fin : hausdorffEDist ∅ ∅ ≠ ∞
⊢ ∅ = ∅ ∧ ∅ = ∅ ∨ ∅.Nonempty ∧ ∅.Nonempty

case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist ∅ t ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
cases le_total δ 0

Goal state after:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : δ ≤ 0
⊢ cthickening (max 0 δ) E = cthickening δ E

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : 0 ≤ δ
⊢ cthickening (max 0 δ) E = cthickening δ E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε

Tactic:
refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_

Goal state after:
case refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε) s) = ∞

case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞

case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S}

pp: case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S} ≤ borel α

Tactic:
· rw [borel_eq_generateFrom_Ioc]
    apply generateFrom_mono (by grind)

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Ioc l u = S} ≤ borel α
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ μ = ν

Tactic:
refine
    ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
      (isPiSystem_Ico (id : α → α) id) ?_ hμν
  rintro - ⟨a, b, hlt, rfl⟩
  exact h hlt

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

Goal state before:
pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
⊢ 0 < η → ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + ↑η

Tactic:
η_pos

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
⊢ ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + ↑η
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
⊢ hausdorffDist s t ≤ r

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ x ∈ ∅, infDist x s ≤ r
⊢ hausdorffDist s ∅ ≤ r

case inr.inr
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, infDist x t ≤ r
H2 : ∀ x ∈ t, infDist x s ≤ r
hs : s.Nonempty
ht : t.Nonempty
⊢ hausdorffDist s t ≤ r
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
h : ∀ (a : α), μ (Iic a) = ν (Iic a)
s : Set α
hsc : s.Countable
hsd : Dense s
hst : ∀ (x : α), IsTop x → x ∈ s
this : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ μ univ = ν univ

Tactic:
simp only [← biSup_measure_Iic hsc (hsd.exists_ge' hst) this, h]

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:
finiteness

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝¹
hD : generateFrom D = inst✝
h2C : IsCountablySpanning C
h2D : IsCountablySpanning D
⊢ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D) = Prod.instMeasurableSpace

Tactic:
by
  rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]

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

Goal state before:
pp: case inl.inr
α : 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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
⊢ Measurable g

Tactic:
have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg

Goal state after:
case inl.inr
α : 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 g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
⊢ Measurable g
Module: Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s✝ : Set α
inst✝ : NullSingletonClass μ
s : Set α
⊢ NullSingletonClass (μ.restrict s)

Tactic:
refine ⟨fun x => ?_⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s✝ : Set α
inst✝ : NullSingletonClass μ
s : Set α
x : α
⊢ (μ.restrict s) {x} = 0
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
← range_add_eq_image_Ici,

Goal state after:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone fun n ↦ f (n + k)
h_bdd : BddAbove (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sSup (range fun x ↦ f (x + k))))
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
← range_add_eq_image_Ici,

Goal state after:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone fun n ↦ f (n + k)
h_bdd : BddBelow (range fun x ↦ f (x + k))
⊢ Tendsto (fun n ↦ f (n + k)) atTop (𝓝 (sInf (range fun x ↦ f (x + k))))
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ f.lintegral μ ≤ f.lintegral ν

Tactic:
simp only [lintegral]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) ≤ ∑ x ∈ f.range, x * ν (⇑f ⁻¹' {x})
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | c (rs a) ≤ f n a}
n : ℕ
a : α
⊢ ((SimpleFunc.map c rs).restrict {a | (SimpleFunc.map c rs) a ≤ f n a}) a ≤ f n a

Tactic:
simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]

Goal state after:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | c (rs a) ≤ f n a}
n : ℕ
a : α
⊢ {a | c (rs a) ≤ f n a}.indicator (c ∘ ⇑rs) a ≤ f n a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, μ {x | ε ≤ f x} = 0
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), u n ∈ Ioo 0 1
tu : Tendsto u atTop (𝓝 0)
u_union : {x | f x ≠ 0} = ⋃ n, {x | u n ≤ f x}
res : μ (⋃ i, {x | u i ≤ f x}) = 0
⊢ f =ᵐ[μ] 0

Tactic:
rwa [← u_union] at res

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ∞} ≠ 0
⊢ μ {x | x ∈ s ∧ f x = ∞} ≤ (μ.restrict s) {x | f x = ∞}

Tactic:
rw [← ofPred_inter_eq_sep]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ∞} ≠ 0
⊢ μ ({a | f a = ∞} ∩ s) ≤ (μ.restrict s) {x | f x = ∞}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
simp only [lintegral]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ s.indicator f a), g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ f a), g.lintegral (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
⊢ StronglyMeasurable f

Tactic:
let f_approx : ℕ → @SimpleFunc α m β := fun n =>
    @SimpleFunc.mk α m β
      (hf.approx n)
      (fun x => h_mono _ (SimpleFunc.measurableSet_fiber' _ x))
      (SimpleFunc.finite_range (hf.approx n))
  exact ⟨f_approx, hf.tendsto_approx⟩

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

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

Tactic:
exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ

Tactic:
simp only [lintegral]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ (⨆ g, ⨆ (_ : ⇑g ≤ fun a ↦ f a), g.lintegral μ) + ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ g a), g_1.lintegral μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a + g a), g_1.lintegral μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)

Tactic:
refine ⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩  ↦ ?_⟩
  have := Hsep.secondCountableTopology
  have Hm' : StronglyMeasurable (rangeFactorization f) := Hm.subtype_mk.stronglyMeasurable
  exact continuous_subtype_val.comp_stronglyMeasurable Hm'

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
simpa only [add_comm] using lintegral_add_left' hg f

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [lintegral, ENNReal.mul_iSup]
  refine iSup_le fun s => ?_
  rw [ENNReal.mul_iSup, iSup_le_iff]
  intro hs
  rw [← SimpleFunc.const_mul_lintegral, lintegral]
  refine le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)
  dsimp
  grw [hs x]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ

Tactic:
simp only [(mul_assoc _ _ _).symm, rinv'] at this

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), 1 * f a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
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)
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))

Tactic:
filter_upwards [h_exists] with a ha

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 : α
ha : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s ↦ ∑ b ∈ s, f b

Tactic:
exact cauchySeq_finset_of_norm_bounded hg h

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
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)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds (↑K * 0))

Tactic:
exact blim.const_mul _

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_3
α : 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)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds (↑K * 0))

Tactic:
exact blim.const_mul _

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
h : a ≤ b
this : ∀ {c d : α}, d ≤ c → |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
hdc : ¬d ≤ c
⊢ |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Tactic:
rw [abs_sub_comm, abs_sub_comm c]; exact this (le_of_not_ge hdc)

Goal state after: