mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x ↦ ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ motive f

Tactic:
refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf
  convert!
    iSup (f := fun n ↦ (s ∩ spanningSets μ n).indicator fun _ ↦ c)
      (fun n ↦ measurable_const.indicator (hs.inter (measurableSet_spanningSets ..)))
      (fun m n hmn a ↦ by dsimp; grw [hmn])
      (fun n ↦
        indicator _ (hs.inter (measurableSet_spanningSets ..))
          (measure_inter_lt_top_of_right_ne_top (measure_spanningSets_lt_top ..).ne)) with
    a
  simp [← Set.indicator_iUnion_apply (M := ℝ≥0∞) rfl, ← Set.inter_iUnion]

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

Goal state before:
pp: α : 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
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᵐ[μ] f
⊢ AEStronglyMeasurable f μ

Tactic:
suffices StronglyMeasurable[m'] (s.indicator (hf.mk f)) from
    this.aestronglyMeasurable.congr h_ind_eq

Goal state after:
α : 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
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᵐ[μ] f
⊢ StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case pos
α : 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:
let ψ := φ.map ENNReal.toNNReal

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ∀ᵐ (a : α) ∂μ, φ a ≠ ∞
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ∫⁻ (a : α), ⨅ i, ⨅ h, f i h a ∂μ ≤ ⨅ i, ⨅ h, ∫⁻ (a : α), f i h a ∂μ

Tactic:
convert! (monotone_lintegral μ).map_iInf₂_le f with a

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ ⨅ i, ⨅ h, f i h a = (⨅ i, ⨅ j, f i j) a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
⊢ ⨆ n, ((SimpleFunc.map c rs).restrict {a | (SimpleFunc.map c rs) a ≤ f n a}).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp only [← SimpleFunc.lintegral_eq_lintegral]
      gcongr with n a
      simp only [map_apply] at h_meas
      simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]
      exact indicator_apply_le id

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 α := 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))
⊢ ∃ n, ∀ (m_1 : ℕ), n ≤ m_1 → (fs m_1) x = (f_approx m_1) x

Tactic:
obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial

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))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
⊢ ∃ n, ∀ (m_1 : ℕ), n ≤ m_1 → (fs m_1) x = (f_approx m_1) x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ = c * μ s

Tactic:
rw [lintegral_indicator₀ hs, setLIntegral_const]

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

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

Tactic:
intro hsσ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ∞

Tactic:
exact measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
    have := hC.acc _ yC
    rw [accPt_iff_nhds] at this
    rcases this univ univ_mem with ⟨x, xC, hxy⟩
    exact ⟨x, xC.2, hxy⟩

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : 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
⊢ CauchySeq (f ∘ u)

Tactic:
by
  rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
  refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
  · exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
  · intro n m N hn hm
    have A n : u n ∈ s := h'u (mem_range_self _)
    apply (hf.dist_le_mul _ (A n) _ (A m)).trans
    exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2
  · rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I → t ∈ Icc 0 (1 / a)

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mp
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ∈ Icc 0 (1 / a)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mpr
a t : ℝ
ha : 0 < a
⊢ t ∈ Icc 0 (1 / a) → a * t ∈ I

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ∈ I
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp
t : ℝ
⊢ 2 * t - 1 ∈ I → t ∈ Icc (1 / 2) 1

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mp
t : ℝ
h₁ : 0 ≤ 2 * t - 1
h₂ : 2 * t - 1 ≤ 1
⊢ t ∈ Icc (1 / 2) 1
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mpr
t : ℝ
⊢ t ∈ Icc (1 / 2) 1 → 2 * t - 1 ∈ I

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
t : ℝ
h₁ : 1 / 2 ≤ t
h₂ : t ≤ 1
⊢ 2 * t - 1 ∈ I
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ↑s = 1
ht : ¬↑t = 1
⊢ (1 - 1) * ↑x + 1 * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - 1 * ↑t) * ((1 - 1 * (1 - ↑t) / (1 - 1 * ↑t)) * ↑x + 1 * (1 - ↑t) / (1 - 1 * ↑t) * ↑y) + 1 * ↑t * ↑z

Tactic:
· have : (1 - t : ℝ) ≠ 0 := by grind
      field_simp
      simp

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
⊢ ↑y = ↑(convexComb x z ⟨(↑y - ↑x) / (↑z - ↑x), ⋯⟩)

Tactic:
simp only [coe_convexComb]

Goal state after:
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ Sum.dist (Sum.inl p) x✝ ≤ Sum.dist (Sum.inl p) (Sum.inr q) + Sum.dist (Sum.inr q) x✝

Tactic:
by
      simp only [Sum.dist_eq_glueDist p q]
      exact glueDist_triangle _ _ _ (by simp) _ _ _

Goal state after:
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
hδ : 0 < δ / 2
h : 0 ≤ 1
⊢ ∃ 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:
refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩

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
h : 0 ≤ 1
n m : ℕ
⊢ ∃ i,
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr.inr
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
hne : x ≠ y
⊢ dist (f x) (f y) ≤ dist x y

Tactic:
rw [dist_eq_of_ne hne]

Goal state after:
case mpr.inr
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
hne : x ≠ y
⊢ dist (f x) (f y) ≤ (1 / 2) ^ firstDiff x y
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := ⋯
⊢ ⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1 = Icc a b

Tactic:
rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : ↑(Icc 0 1) ≃ₜ ↑(⇑(affineHomeomorph (b - a) a ⋯) '' Icc 0 1) := (affineHomeomorph (b - a) a ⋯).image (Icc 0 1)
⊢ Icc a (b - a + a) = Icc a b
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ let D := closure (eball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ ediam D ≤ ε

Tactic:
refine ⟨this.1, this.2, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ closure (eball x (ε / 2) ∩ C) ⊆ C

case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (closure (eball x (ε / 2) ∩ C)) ≤ ε
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y

Tactic:
rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set ↑s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : ↑s) in t, f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ

Tactic:
by
  rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ∀ (i : ι), (μ i) (⋂ b, s b) = 0

Tactic:
exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)

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

Goal state before:
pp: case hd
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)

pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
· exact Disjoint.mono inter_subset_right inter_subset_right disjoint_compl_right

Goal state after:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s

Tactic:
rw [hμ, ae_finsetSum_measure_iff]

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ {i} • dirac i, x ∈ s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ (∀ᵐ (y : α) ∂map f μ, y ∈ s) ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a

Tactic:
ae_mem_finset_iff

Goal state after:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
f : β → α
s : Finset α
μ : Measure β
hf : AEMeasurable f μ
⊢ map f μ = ∑ a ∈ s, (map f μ) {a} • dirac a ↔ map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • dirac a
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : μ Fᶜ = 0
⊢ F = univ

Tactic:
hF.isOpen_compl.measure_eq_zero_iff μ,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : Fᶜ = ∅
⊢ F = univ
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ ↑C ^ n * μ (closedBall x (2 * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
hε,

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ ↑C ^ n * (↑(doublingConstant μ) * μ (closedBall x ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν

Tactic:
simp only [← indicator_comp_right]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ∫⁻ (y : β), (Prod.mk x ⁻¹' s).indicator ((fun x ↦ c) ∘ Prod.mk x) y ∂ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case neg.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL✝ : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ¬∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ L < ∫⁻ (x : α), ↑((g₁ + g₂) x) ∂μ

Tactic:
apply hL.trans ((ENNReal.add_lt_add hg₁ hg₂).trans_le _)
      rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
      simp only [coe_add, Pi.add_apply, ENNReal.coe_add, le_rfl]

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

Goal state before:
pp: X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')

Tactic:
use s ×ˢ t, Filter.prod_mem_prod hs ht

Goal state after:
case right
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : μ s < ∞
t : Set Y
ht : t ∈ l'
hνt : ν t < ∞
⊢ (μ.prod ν) (s ×ˢ t) < ∞
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝¹
hD : generateFrom D = inst✝
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t
⊢ μ.prod ν = μν

Tactic:
refine
    (h3C.prod h3D).ext
      (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm
      (h2C.prod h2D) ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst✝¹
hD : generateFrom D = inst✝
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t
⊢ ∀ s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D, (μ.prod ν) s = μν s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : α × β) ∂μ.prod ν, p x.1 x.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
by rw [← prod_swap, ae_map_iff (by fun_prop) h]; simp

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

Goal state before:
pp: γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ

Tactic:
refine le_antisymm ?_ (borel_anti hle)

Goal state after:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ ≤ borel γ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
⊢ (∑ i ∈ ∅, μ i).InnerRegular

Tactic:
simp only [Finset.sum_empty]

Goal state after:
case empty
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
⊢ InnerRegular 0