mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
n : ℕ
⊢ ∃ m, s m ⊆ dissipate s n

Tactic:
by
  induction n with
  | zero => use 0; simp [dissipate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    exact ⟨k, by simp; grind⟩

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
· by_cases! Hu : ∃ u, f x < u
    · rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
      filter_upwards [h₂ u fxu] with a lfa
      apply hu
      exact ⟨Hl (f a), lfa⟩
    · apply Filter.Eventually.of_forall
      intro a
      have : f a = f x := le_antisymm (Hu _) (Hl _)
      rw [this]
      exact mem_of_mem_nhds hv

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
⊢ m.IsCaratheodory ∅

Tactic:
simp [IsCaratheodory, sdiff_empty]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + m (t \ s₁) = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))

Tactic:
h₂ (t \ s₁),

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
· simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄
    exact continuousAt_mul_top_ne_zero h₄

Goal state after:
case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∀ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
intro b h_b
    simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b
    obtain ⟨h_b_w, h_b_h⟩ := h_b
    have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
    rw [h_b_alt, Subtype.val_injective.extend_apply]
    apply h_t'
    apply h_b_h

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = f i x

Tactic:
by
  simp only [aeSeq_eq_mk_of_mem_aeSeqSet hf hx i, mk_eq_fun_of_mem_aeSeqSet hf hx i]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.domRestrict (extend f g g'))

Tactic:
rw [domRestrict_extend_compl_range]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ ((restrict s) μ.trim) t

Tactic:
rw [restrict_apply]
    rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩
    rw [← hμt']
    rw [inter_subset] at htt'
    refine (measure_mono htt').trans ?_
    rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
      Set.empty_union]
    exact measure_mono inter_subset_left

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

Goal state before:
pp: case refine_1.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
⊢ MeasurableSet (F^[0] univ)

Tactic:
exact MeasurableSet.univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' s)

Tactic:
hft,

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ μ (toMeasurable μ (f ⁻¹' s)) = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict (s ∪ sᶜ) = μ

Tactic:
union_compl_self,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict univ = μ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : μ.restrict s = ν.restrict s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ μ t = ν t

Tactic:
by
    rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : ⋃ i ∈ S, s i = univ
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)

Tactic:
by
  rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))

Tactic:
have h_meas (t) (ht : t ∈ measurableAtom '' s) : MeasurableSet t := by
    obtain ⟨x, hxs, hx⟩ := ht
    rw [← hx]
    exact MeasurableSet.measurableAtom_of_countable x

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
hd : T.Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = sum fun i ↦ μ.restrict (s ↑i)

Tactic:
Set.biUnion_eq_iUnion

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
T : Set ι
hT : Countable ↑T
hd : T.Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ x, s ↑x) = sum fun i ↦ μ.restrict (s ↑i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ✝ : ∀ s ∈ S, μ s < ∞
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), μ (s n) < ∞
hs : ⋃ n, s n = univ
⊢ SigmaFinite μ

Tactic:
exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩

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

Goal state before:
pp: case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet univ

Tactic:
exact MeasurableSet.univ

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
by
  constructor
  · intro h
    exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)
  · intro h
    refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
    have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
    have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
    exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

Goal state after:
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 α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
⊢ MeasurableEq E

Tactic:
by
  constructor
  simp_rw +singlePass [Set.diagonal, ← sub_eq_zero]
  measurability

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

Goal state before:
pp: α✝ : 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
this : Measurable fun p ↦ p.2 • p.1
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by apply this.comp measurable_swap

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

Goal state before:
pp: α✝ : 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✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
this : Measurable fun p ↦ p.2 • p.1
⊢ Measurable (Function.uncurry fun x1 x2 ↦ x1 • x2)

Tactic:
by apply this.comp measurable_swap

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ infEDist x s + ediam s

Tactic:
simp_rw [infEDist, ENNReal.iInf_add]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + ediam s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ n, F n = U

Tactic:
show ⋃ n, F n = U
    refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
    have : x ∉ Uᶜ := by simpa using hx
    rw [mem_iff_infEDist_zero_of_closed hU.isClosed_compl] at this
    have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this
    have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
      ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one
    rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
    simp only [mem_iUnion]
    exact ⟨n, hn.le⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : ↑ε / 2 ≠ 0
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + ↑ε

Tactic:
have : infEDist x s < infEDist x s + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : ↑ε / 2 ≠ 0
this : infEDist x s < infEDist x s + ↑ε / 2
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + ↑ε
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]
  nth_rw 2 [edist_comm]
  exact max_self _

Goal state after:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case e'_2
q : ℚ
⊢ closure (Rat.cast '' {x | q < x}) = closure (Ioi ↑q ∩ range Rat.cast)

pp: case e'_3
q : ℚ
⊢ {r | ↑q ≤ r} = closure (Ioi ↑q)

pp: q : ℚ
⊢ (Ioi ↑q).Nontrivial

Tactic:
· congr!; aesop

Goal state after:
case e'_3
q : ℚ
⊢ {r | ↑q ≤ r} = closure (Ioi ↑q)

q : ℚ
⊢ (Ioi ↑q).Nontrivial
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))

Tactic:
exact isLUB_csSup (image_nonempty.mpr nonempty_Ici) h_bdd

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

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

Tactic:
simp [Set.preimage, hf]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ ∀ (y : ℝ≥0∞), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞

Tactic:
rw [← finMeasSupp_iff]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → ℝ≥0∞ := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᵐ[μ] aeSeqLim

Tactic:
· exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).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_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ⨆ s, ∑ i ∈ s, f i x) μ

Tactic:
exact .iSup fun s ↦ Finset.aemeasurable_fun_sum s fun i _ => h i

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

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

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, ⊥).1 * (↑r, ⊥).2

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:
· exact (measurable_const_mul _).comp measurable_coe_real_ereal

Goal state after:
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

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, ⊥).1 * (↑r, ⊥).2

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

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, ⊥).1 * (↑r, ⊥).2

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:
· exact (measurable_const_mul _).comp measurable_coe_real_ereal

Goal state after:
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, ⊥).1 * (↑r, ⊥).2

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
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
x : α
⊢ ∃ i, x ∈ norm_sets i

Tactic:
exact exists_nat_ge (f x)

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

Goal state before:
pp: α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ μ s = μ (s ∩ f ⁻¹' univ)

Tactic:
preimage_univ,

Goal state after:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ μ s = μ (s ∩ univ)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t_sep : IsSeparable ∅
ht : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEStronglyMeasurable f μ

pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ AEStronglyMeasurable f μ

Tactic:
· simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht
    rw [ht]
    exact aestronglyMeasurable_zero_measure f

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ AEStronglyMeasurable f μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a

Tactic:
ae_restrict_iff₀

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
⊢ ∫⁻ (a : α), f a ∂(μ.restrict (A ∩ B) + μ.restrict (A \ B)) = ∫⁻ (x : α) in A, f x ∂μ

Tactic:
restrict_inter_add_sdiff _ hB

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
⊢ ∫⁻ (a : α) in A, f a ∂μ = ∫⁻ (x : α) in A, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
by
  rw [lintegral_eq_iSup_eapprox_lintegral hf]
  exact le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

Goal state after: