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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ a, s (x a)) = ⨆ i, μ (s i)

Tactic:
← Monotone.iSup_comp_tendsto_atTop _ hx

Goal state after:
case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ a, s (x a)) = ⨆ a, μ (s (x a))

α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Monotone fun i ↦ μ (s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal

Tactic:
suffices (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal by
    rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
    convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ 0
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
← μ.restrict_apply_self,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : (μ.restrict s) s ≠ 0
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ μ s = ν s

Tactic:
induction s, hs using induction_on_inter hA hC with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace β
h : CountablyGenerated β
f : α → β
⊢ CountablyGenerated α

Tactic:
rcases h with ⟨⟨b, hbc, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume univ = volume u

Tactic:
rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]
  · simp only [image_univ, Subtype.range_coe_subtype, ofPred_mem_eq]
  · exact Subtype.coe_injective
  · exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ s.indicator f =ᵐ[μ] s.indicator g

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
n : ℕ
⊢ μ (f ⁻¹' spanningSets (Measure.map f μ) n) < ∞

Tactic:
simp only [← map_apply_of_aemeasurable hf, measurableSet_spanningSets,
          measure_spanningSets_lt_top]

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

Goal state before:
pp: case inl
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g (μ.restrict (Ioc x (u n)))

Tactic:
exact g_meas (u n) h

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ.cofinite ≤ ae μ

Tactic:
intro s hs
  simp_all [mem_cofinite, mem_ae_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
h : IsGδ s
⊢ MeasurableSet s

Tactic:
by
  rcases h with ⟨S, hSo, hSc, rfl⟩
  exact MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet

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

Goal state before:
pp: α : 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 δ
a : α
i : Subtype (Membership.mem {s | a ∈ s ∧ IsOpen[inst✝¹²] s})
⊢ (𝓟 ↑i).IsMeasurablyGenerated

Tactic:
exact i.2.2.measurableSet.principal_isMeasurablyGenerated

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)

Tactic:
rw [← compl_Ioi]

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ
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 : α
x✝ : ∃ i ≤ x, i ≤ b ∧ i ∈ t ∧ x ≤ b
y : α
yx : y ≤ x
hy1 : y ≤ b
hy2 : y ∈ t
hy : x ≤ b
⊢ x < a

Tactic:
by order

Goal state after:
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
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ z ≤ b

Tactic:
by order

Goal state after:
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
this : x ≤ b
z : α
hzt : z ∈ t
hzx : z ≤ x
⊢ x ≤ b

Tactic:
by order

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

Goal state before:
pp: ι : Type u_6
X : ι → Type u_7
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), BorelSpace (X i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → X i)

Tactic:
have : ‹∀ i, MeasurableSpace (X i)› = fun i => borel (X i) :=
    funext fun i => BorelSpace.measurable_eq

Goal state after:
ι : Type u_6
X : ι → Type u_7
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : ∀ (i : ι), BorelSpace (X i)
this : inst✝¹ = fun i ↦ borel (X i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → X i)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹¹ : TopologicalSpace α✝
mα : MeasurableSpace α✝
inst✝¹⁰ : BorelSpace α✝
mβ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : MeasurableSpace δ
α : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : DiscreteTopology α
inst✝¹ : MeasurableSpace α
inst✝ : DiscreteMeasurableSpace α
⊢ BorelSpace α

Tactic:
constructor; ext; simp [MeasurableSpace.measurableSet_generateFrom, MeasurableSet.of_discrete]

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

Goal state before:
pp: δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ (∃ z ∈ E, edist x z < ENNReal.ofReal δ) ↔ ∃ z ∈ E, dist x z < δ

Tactic:
key_iff

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Tactic:
refine (continuous_infDist_pt s).continuousAt.inv₀ ?_

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ infDist x s ≠ 0
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
⊢ ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ = ⋃ x ∈ E, closedBall x δ

Tactic:
hE.closure_eq

Goal state after:
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
⊢ ⋃ x ∈ E, closedBall x δ = ⋃ x ∈ E, closedBall x δ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
this : (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x}
⊢ MeasurableSet ((⨆ i, f i) ⁻¹' Ioi c)

Tactic:
by
    rw [this]
    exact .biUnion cJ fun j _ ↦ by measurability

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ ⨆ n, (approx i f n) a

Tactic:
refine le_iSup_of_le (k + 1) ?_
    rw [approx_apply a hf]
    have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
    refine le_trans (le_of_eq ?_) (Finset.le_sup this)
    rw [if_pos hk]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ n, (eapprox f n) a = f a

Tactic:
eapprox,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ n, (approx ennrealRatEmbed f n) a = f a
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet (Iic ↑q)

Tactic:
rw [← compl_Ioi]

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Ioi ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b})

Tactic:
convert! isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
  ext x
  simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ edist y₀ (f x) + edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x) + edist y₀ (f x)

Tactic:
grw [edist_approxOn_le hf h₀ x n]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ⨆ n, ∫⁻ (a : α), aeSeq hf p n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr with n

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
n : ℕ
⊢ ∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᵐ[μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
rw [← lintegral_add_right' _ hg]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᵐ[μ] f
⊢ ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

Tactic:
by
  rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]

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

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

Tactic:
by
      congr; funext a
      rw [ENNReal.iSup_add_iSup_of_monotone]
      · simp only [Pi.add_apply]
      · intro i j h
        exact monotone_eapprox _ h a
      · intro i j h
        exact monotone_eapprox _ h a

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ∞
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, ↑M ∂μ < ∞

Tactic:
simp [ENNReal.mul_lt_top, hs.lt_top]

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

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
congr with n

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
n : ℕ
⊢ ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a ≤ g a}

Tactic:
borelize (E × E)

Goal state after:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a ≤ g a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet {a | f a = g a}

Tactic:
borelize (E × E)

Goal state after:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace (E × E) := borel (E × E)
this✝ : BorelSpace (E × E)
⊢ MeasurableSet {a | f a = g a}
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
AccPt,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 (U ∩ C)).NeBot
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ AccPt x (𝓟 C)

Tactic:
AccPt,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
VD

Goal state after:
case left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C

Tactic:
VD

Goal state after:
case right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∑' (i : { x // x ∉ n }), ‖f (↑i) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a

Tactic:
apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)

Goal state after:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
⊢ ∀ (i : { x // x ∉ n }), ((fun n ↦ ‖f n x‖) ∘ Subtype.val) i ≤ (u ∘ Subtype.val) i
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 0)

Tactic:
· rw [← mul_zero (K : ℝ)]
    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 0)

Tactic:
· rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
⊢ TopologicalSpace.PseudoMetrizableSpace X

Tactic:
by
  let := upgradeIsCompletelyPseudoMetrizable X
  infer_instance

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1

Tactic:
obtain h | h := eq_or_ne x y

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
h : x = y
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1

case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
h : x ≠ y
⊢ (if x = y then 0 else 1) = if y = x then 0 else 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i

Tactic:
intro hi j hj

Goal state after:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff x y
j : ℕ
hj : j < i
⊢ x j = y j