mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ∃ m, ↑a * ↑n ≤ ↑m

Tactic:
use m

Goal state after:
case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ↑a * ↑n ≤ ↑m
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
coe_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)

Tactic:
classical
  refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe

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

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ ⊥), 𝓟 (Iio a)

Tactic:
simp only [bot_lt_iff_ne_bot]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)
⊢ Tendsto (fun n ↦ ↑(C.toReal / ↑n)) atTop (𝓝 0)

Tactic:
← coe_zero,

Goal state after:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)
⊢ Tendsto (fun n ↦ ↑(C.toReal / ↑n)) atTop (𝓝 ↑0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ 0 < limsup u f ∨ liminf v f ≠ ⊤

Tactic:
refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h : limsup u f ≠ 0
⊢ 0 ≤ limsup u f
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (s : Set α), μ s ≤ ⨆ (_ : s.Nonempty), m s) ↔ ∀ (s : Set α), μ s ≤ m s

Tactic:
forall_congr'

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (a : Set α), ?m.19 a) ↔ ∀ (s : Set α), μ s ≤ m s

α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ ⨆ (_ : a.Nonempty), m a ↔ ?m.19 a

α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ Set α → Prop
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (s : Set α), μ s ≤ m s) ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

Tactic:
forall_congr'

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (a : Set α), ?m.15 a) ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ m a ↔ ?m.15 a

α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ Set α → Prop
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] s

Tactic:
convert! ae_eq_set_inter (ae_eq_refl s) h
  rw [inter_univ]

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 = AEMeasurable.mk (f i) ⋯ x

Tactic:
by
  simp only [aeSeq, hx, if_true]

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ MeasurableSet s ↔
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
by
  rw [isCaratheodory_iff_le]
  constructor
  · intro h t _ht
    exact h t
  · intro h u
    conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
    refine le_iInf ?_
    intro t
    refine le_iInf ?_
    intro ht
    refine le_iInf ?_
    intro h2t
    refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)
    gcongr

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t

Tactic:
rintro (rfl | rfl | rfl | rfl)

Goal state after:
case mpr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = ∅

case mpr.inr.inl
α : Type u_1
t : Set α
⊢ ∃ s', (fun x ↦ x ∈ t) ⁻¹' s' = t

case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2
α✝ : 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 γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable
    (((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inr) univ).symm) ∘
      ⇑(Set.rangeInr.prodCongr (Set.univ γ)).symm)

Tactic:
exact measurable_inr

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), (μs i) s = 0
⊢ ν s = 0

Tactic:
exact hνμ (hs0 i)

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
hs : ∑' (i : ℕ), μ (s i) ≠ ∞
⊢ μ (limsup s cofinite) = 0

Tactic:
measure_limsup_cofinite_eq_zero hs

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
hs : ∑' (i : ℕ), μ (s i) ≠ ∞
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ ({ toFun := fun μ ↦ ((OuterMeasure.restrict s) μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯, map_smul' := ⋯ }
        μ).toOuterMeasure =
    (OuterMeasure.restrict s) μ.toOuterMeasure

Tactic:
LinearMap.coe_mk,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ ({ toFun := fun μ ↦ ((OuterMeasure.restrict s) μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯ } μ).toOuterMeasure =
    (OuterMeasure.restrict s) μ.toOuterMeasure
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅

Tactic:
apply subset_antisymm _ (empty_subset _)

Goal state after:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i ⊆ ∅
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∃ s, x ∈ s ∧ IsOpen[inst✝¹] s ∧ μ s < ∞

Tactic:
by
  simpa only [and_assoc] using (μ.finiteAt_nhds x).exists_mem_basis (nhds_basis_opens x)

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ ⋃ i, f i = univ

Tactic:
refine eq_univ_of_forall fun x => ?_

Goal state after:
case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
x : α
⊢ x ∈ ⋃ i, f i
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ (μ.trim hm₂) t = μ t

Tactic:
trim_measurableSet_eq hm₂ (hm₁₂ t ht)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ μ t = μ t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure

Tactic:
by rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]

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

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated β γ

Tactic:
have := countable_right_of_prod_of_nonempty h

Goal state after:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable β
⊢ CountableOrCountablyGenerated β γ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ) s = (∑ i, μ i) s

Tactic:
simp only [sum_apply, finsetSum_apply, hs, tsum_fintype]

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
⊢ AEMeasurable f μ

Tactic:
obtain ⟨f', hf'm, hf't, hff'⟩ :
        ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
      h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne

Goal state after:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → β
hf'm : NullMeasurable f' μ
hf't : range f' ⊆ t
hff' : f =ᵐ[μ] f'
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Ioi a)

Tactic:
rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy

Goal state after:
case refine_1.inl.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a b : α
hb : a ⋖ b
⊢ MeasurableSet (Ioi a)

case refine_1.inl.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ b, a ⋖ b
⊢ MeasurableSet (Ioi a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hb : Ioo b a = ∅
hbs : b ∈ s
x : α
h : x < a
⊢ x ≤ b

Tactic:
contrapose! hb

Goal state after:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
b : α
ba : b < a
hbs : b ∈ s
x : α
h : x < a
hb : b < x
⊢ (Ioo b a).Nonempty
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

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

Tactic:
· rcases H1 x xs with ⟨y, yt, hy⟩
    exact le_trans (infEDist_le_edist_of_mem yt) hy

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : ENNReal.ofReal δ ≤ infEDist y E
⊢ ENNReal.ofReal δ ≤ edist x y

Tactic:
simpa only [edist_comm] using le_trans hy <| Metric.infEDist_le_edist_of_mem x_in_E

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

Goal state before:
pp: q : ℚ
⊢ ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal

Tactic:
rw [ennrealRatEmbed, Encodable.encodek]

Goal state after:
q : ℚ
⊢ ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ b ∈ f.range

Tactic:
mem_range,

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ b ∈ range ⇑f
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < min z (x + ε)
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
rw [lt_min_iff] at h₂

Goal state after:
case refine_2
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < ↑q
h₂ : ↑q < z ∧ ↑q < x + ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ

Tactic:
map_fst_pair

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ = f.lintegral μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
⊢ AEMeasurable g μ

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ AEMeasurable g μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this

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

Goal state before:
pp: case refine_1
α : 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}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
n : ℕ
⊢ MeasurableSet (sigma_finite_sets n)

Tactic:
exact measurableSet_spanningSets μ n

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ∞
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
· have h_meas : μ (φ ⁻¹' {∞}) ≠ 0 := mt measure_eq_zero_iff_ae_notMem.1 h
    refine le_trans le_top (ge_of_eq <| iSup_eq_top.2 fun b hb => ?_)
    obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)
    use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞})
    simp only [lt_iSup_iff, exists_prop, coe_restrict, φ.measurableSet_preimage, coe_const,
      ENNReal.coe_indicator, map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_natCast,
      restrict_const_lintegral]
    refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩
    simp only [mem_preimage, mem_singleton_iff] at hx
    simp only [hx, le_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ ∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))

Tactic:
obtain ⟨g, _, hg⟩ :
    ∃ g : α → β, Measurable g ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) :=
    measurable_limit_of_tendsto_metrizable_ae (fun n => (hf n).aemeasurable) h_ae_tendsto

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
g : α → β
left✝ : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᵐ[μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x

Tactic:
exact Eventually.of_forall hgt_zero

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

Goal state before:
pp: α : 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 α := ⋯
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := ⋯
fs : ℕ → α →ₛ β := ⋯
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, x ∈ S n

Tactic:
rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]

Goal state after:
α : 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 : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ x ∈ univ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
rw [Ne, ← Measure.measure_univ_eq_zero] at hμ
  refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_
  simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ ≤ᵐ[μ] bound

Tactic:
intro n
    filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'
    rwa [H'] at H

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

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

Tactic:
congr
      funext a
      rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]
      simp

Goal state after: