mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
⊢ Measurable g

Tactic:
suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this

Goal state after:
case inr
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
⊢ ∀ (b : δ), IsLUB {a | ∃ i, f' i b = a} (g b)
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:
lt_min_iff

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.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Encodable ↑s
H : ¬∀ (i : ι), i ∈ s
⊢ Measurable fun b ↦ ⨆ i ∈ s, f i b

Tactic:
have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ :=
      fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H
    simp only [this]
    apply Measurable.sup _ measurable_const
    exact .iSup (fun (i : s) ↦ hf i i.2)

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : Zero β
μ : Measure α
f : α →ₛ β
h : f.FinMeasSupp μ
y : β
hy : y ≠ 0
⊢ ⇑f ⁻¹' {y} ⊆ {x | (fun x ↦ f x = 0 x) x}ᶜ

Tactic:
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx

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

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Ioi ↑a) = generateFrom (⋃ a, {Iic ↑a})

Tactic:
iUnion_singleton_eq_range

Goal state after:
⊢ generateFrom (range fun a ↦ Ioi ↑a) = generateFrom (range fun a ↦ Iic ↑a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ borel ℝ = generateFrom (⋃ a, {Ici ↑a})

Tactic:
borel_eq_generateFrom_Iio_rat,

Goal state after:
⊢ generateFrom (⋃ a, {Iio ↑a}) = generateFrom (⋃ a, {Ici ↑a})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: ⊢ generateFrom (range fun a ↦ Iio ↑a) = generateFrom (⋃ a, {Ici ↑a})

Tactic:
iUnion_singleton_eq_range

Goal state after:
⊢ generateFrom (range fun a ↦ Iio ↑a) = generateFrom (range fun a ↦ Ici ↑a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case neg
α : 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
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ ⋯.some) atTop (𝓝 ⋯.some)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ ⋯.some) atTop (𝓝 ⋯.some)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ ∫⁻ (x : α) in s, c ∂μ = c * μ s

Tactic:
rw [lintegral_const, Measure.restrict_apply_univ]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᵐ[μ.restrict sᶜ] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∈ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᵐ[μ.restrict sᶜ] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
· simp [hxs, hx]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᵐ[μ.restrict sᶜ] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
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

Tactic:
rw [min_eq_left _]

Goal state after:
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
⊢ ‖1‖ * ‖(hf.approx n) x‖ ≤ c

α : 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‖
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᵐ[μ] f'
x : α
hx : f x ∈ s
hx' : f x = f' x
⊢ f' x = (f' ⁻¹' s).piecewise f' (fun x ↦ h_nonempty.some) x

Tactic:
exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using! hx)

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

Goal state before:
pp: case neg
α : 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
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α), f a ∂c • μ.restrict s = c • ∫⁻ (a : α) in s, f a ∂μ

Tactic:
lintegral_smul_measure

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
f : α → ℝ≥0∞
s : Set α
⊢ c • ∫⁻ (a : α) in s, f a ∂μ = c • ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : Measurable fun x ↦ ¬f x = 0
h : f x = 0
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

Tactic:
rw [biUnion_eq_iUnion, lintegral_iUnion₀ (SetCoe.forall'.1 hm) (hd.subtype _ _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), ⨅ n, (f ∘ Directed.sequence f h_directed) n a ∂μ =
    ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | ¬g x = 0}
h : g x = 0
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
← ofReal_norm

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
by
  rw [← lintegral_trim_ae hm]
  all_goals rw [← restrict_trim hm _ hs]
  exact hf.restrict

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

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

Goal state before:
pp: case inr
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_tendsto : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
· exact h_tendsto

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: case pos
ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ₑ ≤ a

pp: case neg
ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ₑ ≤ a

Tactic:
· exact hf.hasSum.enorm_le_of_bounded hg h

Goal state after:
case neg
ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ₑ ≤ a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : Tendsto (fun i ↦ f i a) atTop atBot
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
refine ⟨0, h.mono_right ?_⟩

Goal state after:
case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone fun i ↦ f i a
h : Tendsto (fun i ↦ f i a) atTop atBot
⊢ atBot ≤ 𝓝 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < min (firstDiff x y) (firstDiff y z)
⊢ False

Tactic:
lt_min_iff

Goal state after:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ False
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
rintro ⟨hsX, hsY⟩

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
⊢ ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m

Tactic:
intro m hm

Goal state after:
case mp.succ
α : Type u_2
x y : ℕ → α
n : ℕ
ih : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n + 1
⊢ x m = y m
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ n < firstDiff x y

Tactic:
simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ CauchySeq u

Tactic:
rw [Metric.cauchySeq_iff]

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∈ s
⊢ (s ∩ cylinder x (longestPrefix x s)).Nonempty

Tactic:
exact ⟨x, hx, self_mem_cylinder _ _⟩

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

Goal state before:

Tactic:
range (toInductiveLimit I i) ⊆ closure (toInductiveLimit I i '' (hsX i)) :=
      (toInductiveLimit_isometry I i |>.continuous).range_subset_closure_image_dense (hdX i)
    _ ⊆ closure s := closure_mono <| subset_iUnion (fun j ↦ toInductiveLimit I j '' hsX j) i

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : MeasurePreserving g μb μc
hf : MeasurePreserving f μa μb
⊢ map (g ∘ f) μa = μc

Tactic:
by rw [← map_map hg.1 hf.1, hf.2, hg.2]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
· rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

Tactic:
symm

Goal state after:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix y s < firstDiff x y
⊢ cylinder y (longestPrefix y s) = cylinder x (longestPrefix x s)
Module: Mathlib.SetTheory.Cardinal.ENNReal

Goal state before:
pp: α : Type u_1
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

Tactic:
cases finite_or_infinite α

Goal state after:
case inl
α : Type u_1
h✝ : Finite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

case inr
α : Type u_1
h✝ : Infinite α
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (dirac a).restrict s = if a ∈ s then dirac a else 0

Tactic:
by
  split_ifs with has
  · apply restrict_eq_self_of_ae_mem
    rw [ae_dirac_iff] <;> assumption
  · rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : β), (g a) s ∂m.bind f = (m.bind fun a ↦ (f a).bind g) s

Tactic:
lintegral_bind hf,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), (g x) s ∂f a ∂m = (m.bind fun a ↦ (f a).bind g) s

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ AEMeasurable (fun a ↦ (g a) s) (m.bind f)