mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case negSucc
α : Type u_1
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x ↦ (x ^ (n + 1))⁻¹

Tactic:
exact (measurable_id.pow_const (n + 1)).inv

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

Goal state before:
pp: case inter
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u s₁ s₂ : Set α
a✝¹ : GenerateOpen s s₁
a✝ : GenerateOpen s s₂
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
⊢ False

Tactic:
rcases le_or_gt (dist z x) (dist y x) with hle | hlt

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hle : dist z x ≤ dist y x
⊢ False

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s ∩ closedBall x (dist y x)
hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))
z : α
hzs : z ∈ s
hz : dist x z < infDist x (s ∩ closedBall x (dist y x))
hlt : dist y x < dist z x
⊢ False
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y

Tactic:
set t := s ∩ closedBall x (dist z x)

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y ∈ s, infDist x t = dist x y
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E

Tactic:
refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_
  · obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
    have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
    exact ss.trans (thickening_mono hε'.2 E)
  · rw [cthickening_eq_iInter_cthickening' s hsδ hs E]
    exact iInter₂_mono fun ε _ => thickening_subset_cthickening ε E

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

Goal state before:
pp: α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ μ = ν

Tactic:
refine @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_ <;> intro a b hab <;> erw [Ico_toDual (α := α)]

Goal state after:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) ≠ ∞

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (⇑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas

Goal state after:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ⇑f ⁻¹' {x} = ∅ ∨ ⇑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), f x = c
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ ⇑(f.restrict s) ⁻¹' t = s ∩ ⇑f ⁻¹' t

Tactic:
simp [hs, indicator_preimage_of_notMem _ _ ht, inter_comm]

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 ≤ (approx i f (k + 1)) a

Tactic:
approx_apply a hf

Goal state after:
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 ≤ (Finset.range (k + 1)).sup fun k ↦ if i k ≤ f a then i k else 0
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 : ι
⊢ Measurable g

Tactic:
· have : Nonempty ι := ⟨i⟩
    let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
    suffices ∀ b, IsLUB { a | ∃ i, f' i b = a } (g b) from
      Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
    intro b
    by_cases hb : b ∈ s
    · have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
      simpa [A] using hg b hb
    · have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
      simp [A, hg' hb, isLUB_singleton]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Goal state after:
case inl
α : 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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : IsEmpty α
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}

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 : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)

Tactic:
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
    ENNReal.tsum_mul_left]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ ∑' (x : ↥f.range) (i : ι), ↑x * (μ i) (⇑f ⁻¹' {↑x}) = ∑' (i : ι) (x : ↥f.range), ↑x * (μ i) (⇑f ⁻¹' {↑x})
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:
← 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: a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (Ioi a)

Tactic:
rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]

Goal state after:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) L (𝓝 l)
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x))

Tactic:
inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using hx

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x

Tactic:
push Not at h

Goal state after:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x
⊢ edist (e ((nearestPtInd e N) x)) x ≤ edist (e k) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a | f a < g a} μ

Tactic:
apply
    (hf.stronglyMeasurable_mk.measurableSet_lt hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᵐ[μ] {a | f a < g a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c

case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x ↦ c
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

Tactic:
simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ⨆ x, ((↑x).restrict s).lintegral μ ≤ ⨆ x, (↑x).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞

Tactic:
rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)]

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

Goal state before:
pp: case intro.inr
α : 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 : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
calc
    ∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
obtain ⟨g, hmg, hgf, hifg⟩ := exists_measurable_le_lintegral_eq (μ := μ) f
  use g, hmg, hgf
  refine fun s hms ↦ le_antisymm ?_ (lintegral_mono hgf)
  rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]
  · gcongr; apply hgf
  · rw [hifg] at hf
    exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)
  · exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

pp: case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ

pp: case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a

Tactic:
· simp [lintegral_finsetSum' _ fun i _ => hf i]

Goal state after:
case hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∀ (b : Finset β), AEMeasurable (fun a ↦ ∑ i ∈ b, f i a) μ

case h_directed
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun s a ↦ ∑ i ∈ s, f i a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ f =ᵐ[μ.trim hm] g

Tactic:
by
  rwa [EventuallyEq, ae_iff, trim_measurableSet_eq hm]
  exact (hf.measurableSet_eq_fun hg).compl

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ μ s = ∞

Tactic:
rw [measure_eq_iInf]
  simp_rw [iInf_eq_top]
  suffices ∀ t, t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → s ⊆ t → MeasurableSet t → μ t = ∞ by
    intro t hts ht
    suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
      measure_mono_top Set.inter_subset_left this
    have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
    exact this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)
  intro t ht_subset hst ht
  refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_
  exact fun hνt ↦ hνs (measure_mono_null hst hνt)

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (U ∩ C)) ∧ (closure[inst✝¹] (U ∩ C)).Nonempty) ∧ closure[inst✝¹] (U ∩ C) ⊆ C

Tactic:
refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩

Goal state after:
case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ closure[inst✝¹] (U ∩ C) ⊆ C
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : α), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]; exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

Tactic:
by
  let := upgradeIsCompletelyPseudoMetrizable Y
  let : PseudoMetricSpace X := hf.isEmbedding.comapPseudoMetricSpace
  have : CompleteSpace X := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
  infer_instance

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

Goal state before:
pp: case mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i

Tactic:
simp [H i h'i, h'i.ne]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set ↑(Icc a b)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
⊢ ∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
have hδ := half_pos δ_pos

Goal state after:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set ↑(Icc a b)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
⊢ ∃ t,
    t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Tactic:
have hδ := half_pos δ_pos

Goal state after:
ι : Sort u_1
c : ι → Set (↑I × ↑I)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
δ : ℝ
δ_pos : δ > 0
ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ t,
    t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
⊢ (∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n) →
    ∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y

Tactic:
intro H x y

Goal state after:
case mpr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
⊢ dist (f x) (f y) ≤ dist x y
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩

Tactic:
simp only [hik, hij, hjk, Sigma.dist_ne, Ne, not_false_iff]

Goal state after:
case inr.inr.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case succ.refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ (inducedMap A).snd x ∈ A (↑x n :: res (↑x) n)

Tactic:
rw [← res_succ]

Goal state after:
case succ.refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
n : ℕ
ih : res (↑x) n = res (↑y) n
hA : ¬↑x n = ↑y n
⊢ (inducedMap A).snd x ∈ A (res (↑x) n.succ)