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

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i).domRestrict g)

pp: case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i)ᶜ.domRestrict g)

pp: case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x

Tactic:
· rw [domRestrict_piecewise]
    simp only [s]
    exact measurable_const

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i)ᶜ.domRestrict g)

case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ Disjoint {k | μ (t' k) ≤ ν (t' k)} {k | ν (t' k) < μ (t' k)}

Tactic:
rw [Set.disjoint_iff]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ {k | μ (t' k) ≤ ν (t' k)} ∩ {k | ν (t' k) < μ (t' k)} ⊆ ∅
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ (map f μ).restrict s = (map (AEMeasurable.mk f hf) μ).restrict s

Tactic:
congr 1

Goal state after:
case e_μ
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ

Tactic:
by
  rw [← biUnion_of_singleton s, compl_iUnion₂]
  exact .biInter hs fun x _ => .compl_singleton x

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst✝²] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i ↦ U i
⊢ IsGδ {x}

Tactic:
← biInter_basis_nhds h_basis.toHasBasis

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst✝²] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i ↦ U i
⊢ IsGδ (⋂ i, ⋂ (_ : True), U i)
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
G : Type u_2
α : Type u_3
β✝ : Type u_4
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β✝
f g : α → G
μ : Measure α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
⊢ MeasurableSet (Set.diagonal β)

Tactic:
simp_rw [Set.diagonal, le_antisymm_iff, ← tsub_eq_zero_iff_le]

Goal state after:
α✝ : Type u_1
G : Type u_2
α : Type u_3
β✝ : Type u_4
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β✝
f g : α → G
μ : Measure α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
⊢ MeasurableSet {p | p.1 - p.2 = 0 ∧ p.2 - p.1 = 0}
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
X : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : SMul M X
m : MeasurableSpace α
μ : Measure α
f : α → M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableSMul M X
hf : AEMeasurable f μ
y : X
⊢ AEMeasurable (fun x ↦ f x • y) μ

Tactic:
by fun_prop

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
⊢ MeasurableSet s

Tactic:
let F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s✝ t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
h : SecondCountableTopologyEither α β
s : Set (α × β)
hs : IsOpen[instTopologicalSpaceProd] s
hβ : SecondCountableTopology β
F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen[inst✝¹²] b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
⊢ MeasurableSet s
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
by
  intro x x_in_E
  simp only [thickening, mem_compl_iff, mem_ofPred_eq, not_lt]
  apply le_infEDist.mpr fun y hy ↦ ?_
  simp only [mem_compl_iff, mem_ofPred_eq, not_lt] at hy
  simpa only [edist_comm] using le_trans hy <| Metric.infEDist_le_edist_of_mem x_in_E

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

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

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · rcases t.eq_empty_or_nonempty with rfl | ht
    · exact Or.inl ⟨rfl, rfl⟩
    · rw [hausdorffEDist_comm] at fin
      exact Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩
  · exact Or.inr ⟨hs, nonempty_of_hausdorffEDist_ne_top hs fin⟩

Goal state after:
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 ∈ t, infDist x s ≤ r

Tactic:
intro x xt
    rcases H2 x xt with ⟨y, ys, hy⟩
    exact le_trans (infDist_le_dist_of_mem ys) hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ ↑(map g f).range = ↑(Finset.image g f.range)

Tactic:
by simp only [coe_range, coe_map, Finset.coe_image, range_comp]

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
x : α
⊢ Measurable (edist x)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
x : α
⊢ Measurable fun y ↦ edist y x

Tactic:
by fun_prop

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✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ Measurable f

Tactic:
apply measurable_of_Ioi

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
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 β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableEmbedding (Prod.map g f)

Tactic:
rw [MeasurableEmbedding.iff_comap_eq]
  refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
  · rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap,
      hg.comap_eq, hf.comap_eq]
  · rw [range_prodMap]
    exact hg.measurableSet_range.prod hf.measurableSet_range

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ Tendsto (fun i ↦ (As i).indicator fun x ↦ b) L (𝓝 (A.indicator fun x ↦ b)) ↔
    Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))

Tactic:
tendsto_indicator_const_iff_forall_eventually _ b,

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝¹ : Mul β
inst✝ : ContinuousMul β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ StronglyMeasurable (AEStronglyMeasurable.mk f hf * AEStronglyMeasurable.mk g hg)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
a✝ : Nontrivial α
g : ℕ → α
hg : Surjective g
⊢ StronglyMeasurable f

Tactic:
exact ⟨simpleFuncAux f g, hg.forall.2 fun m ↦
    tendsto_nhds_of_eventually_eq simpleFuncAux_eventuallyEq⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    ⨆ i ∈ fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x, (SimpleFunc.map ofNNReal i).lintegral μ + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
skip

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    ⨆ i ∈ fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x, (SimpleFunc.map ofNNReal i).lintegral μ + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : ‖(hf.approx n) x‖ ≤ c
⊢ 1 ≤ c / ‖(hf.approx n) x‖

Tactic:
one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))

Goal state after:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : ‖(hf.approx n) x‖ ≤ c
⊢ ‖(hf.approx n) x‖ ≤ c
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg.inl
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : ‖(hf.approx n) x‖ ≤ c
⊢ ‖min 1 (c / ‖(hf.approx n) x‖)‖ * ‖(hf.approx n) x‖ ≤ c

pp: case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖min 1 (c / ‖(hf.approx n) x‖)‖ * ‖(hf.approx n) x‖ ≤ c

Tactic:
· rw [min_eq_left _]
    · simpa only [norm_one, one_mul] using h
    · rwa [one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]

Goal state after:
case neg.inr
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬‖(hf.approx n) x‖ = 0
h : c ≤ ‖(hf.approx n) x‖
⊢ ‖min 1 (c / ‖(hf.approx n) x‖)‖ * ‖(hf.approx n) x‖ ≤ c
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Monotone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ n, f n a ∂μ

Tactic:
refine lintegral_congr_ae ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Monotone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ F =ᵐ[μ] fun a ↦ ⨆ n, f n a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ

Tactic:
by
  rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩
  calc
    ∫⁻ x, f x ∂μ + ε * μ { x | f x + ε ≤ g x } = ∫⁻ x, φ x ∂μ + ε * μ { x | f x + ε ≤ g x } := by
      rw [hφ_eq]
    _ ≤ ∫⁻ x, φ x ∂μ + ε * μ { x | φ x + ε ≤ g x } := by
      gcongr
      exact hφ_le _
    _ = ∫⁻ x, φ x + indicator { x | φ x + ε ≤ g x } (fun _ => ε) x ∂μ := by
      rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
      exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
    _ ≤ ∫⁻ x, g x ∂μ := lintegral_mono_ae (hle.mono fun x hx₁ => ?_)
  simp only [indicator_apply]; split_ifs with hx₂
  exacts [hx₂, (add_zero _).trans_le <| (hφ_le x).trans hx₁]

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∉ s
⊢ s.indicator f a ≤ 1

Tactic:
skip

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∉ s
⊢ s.indicator f a ≤ 1
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ⨆ b, ∫⁻ (a : α), f b a ∂μ = ⨆ b, ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
congr 1

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ (fun b ↦ ∫⁻ (a : α), f b a ∂μ) = fun b ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ f b =ᵐ[μ] aeSeq hf p b

Tactic:
apply EventuallyEq.symm

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := ⋯
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ aeSeq hf p b =ᵐ[μ] f b
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦
    lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Antitone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Antitone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ n, f n a ∂μ

Tactic:
refine lintegral_congr_ae ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Antitone fun n ↦ ∫⁻ (x : α), f n x ∂μ
⊢ F =ᵐ[μ] fun a ↦ ⨅ n, f n a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in s, s.piecewise f g x ∂μ + ∫⁻ (x : α) in sᶜ, s.piecewise f g x ∂μ =
    ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in s, s.piecewise f g x ∂μ = ∫⁻ (a : α) in s, f a ∂μ

case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f g : α → ℝ≥0∞
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ ∫⁻ (x : α) in sᶜ, s.piecewise f g x ∂μ = ∫⁻ (a : α) in sᶜ, g a ∂μ
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, Measurable (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))
⊢ ∀ (a : ι), Measurable (F a) → AEMeasurable (F a) μ

Tactic:
by fun_prop

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

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

Tactic:
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
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
simp only [ball_zero_eq, Set.mem_ofPred_eq]

Goal state after:
Module: Mathlib.Topology.Order.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
a b : α
h : a ≤ b
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ max a (min b x)

Tactic:
by fun_prop

Goal state after: